Need help understanding a proof in Boolos's "The Logic of Provability" I'm currently reading The Logic of Provability by George Boolos and there's a step in a proof that I don't understand.
The author has defined a system of modal logic called GL; its language has a countable collection of sentence letters $p$, $q$, $\ldots$ as well as the symbols $\to$, $\bot$ and $\Box$; sentences are defined inductively in the obvious way (i.e. $\bot$ and each sentence letter $p$ is a sentence, $(A \to B)$ and $\Box A$ are sentences whenever $A$ and $B$ are), $\neg A$ is defined to be $(A \to \bot)$ and $\Diamond A$ is defined to be $\neg \Box \neg A$.
The axioms of GL are all tautologies (although the author hasn't said as much, I assume that the truth of $\Box A$ should be taken as independent of that of any subsentences of $A$ in determining whether something is a tautology) as well as all sentences of the following forms:

$\Box (A \to B) \to (\Box A \to \Box B)$
$\Box (\Box A \to A) \to \Box A $

and its rules of inference are modus ponens and necessitation (i.e. from $A$ infer $\Box A$). It has been proved that all sentences of the form

$\Box A \to \Box \Box A$

are theorems, and that theorems of GL are closed under substitution of arbitrary sentences for sentence letters. The author has also proved Theorem 21 for all $p$:

$\mathrm{GL} \vdash \Box \bot \leftrightarrow \Box \Diamond p$.

A couple of pages later, the author says "by Theorem 21 (with $\bot$ for $p$)

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box \Box (p \leftrightarrow \neg \Box p)$"

I've been scratching my head for a while and I've no idea how he gets this. Can anyone help? 
 A: I still don't know what the author had in mind, but over in sci.logic Daryl McCullough has presented an alternative proof of the statement in question:
From the rule $\Box A \to \Box \Box A$ and distribution we can derive

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box (\Box p \leftrightarrow \Box \neg \Box \bot)$

From Theorem 21 (with $\neg \bot$ for $p$) we have

$\mathrm{GL} \vdash \Box \neg \Box \bot \leftrightarrow \Box \bot$

From both of the above we have

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box (\Box p \leftrightarrow \Box \bot)$

Also by tautology and distribution

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box (\neg p \leftrightarrow \Box \bot)$

From the last two equations,

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box (\Box p \leftrightarrow \neg p)$

The above, together with tautology and distribution, gives

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box (p \leftrightarrow \neg \Box p)$

And again from $\Box A \to \Box \Box A$,

$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box \Box (p \leftrightarrow \neg \Box p)$

