How is this argument of Edward Nelson's not flawed?

Question

Edward Nelson has started writing out the details of a proof of the inconsistency of a version of arithmetic. I'm an undergraduate trying to read through this slowly and carefully.

I've run into a problem, however, with one of his arguments on page 11. It's a proof that "there is a specific number that is not a finite number", which he attributes to Simon Kochen. I did a little digging, and found he had written up a better version of the argument on page 74 of his 1986 book "Predicative Arithmetic" (available on his website). For your convenience, here are just the relevant pages:

My problem is specifically these two sentences:

Let $D$ be the unary formula $C[n] \rightarrow \forall n C[n]$. Then $\exists n D[n]$ is provable, since it is equivalent to the tautology $\forall n C[n] \rightarrow \forall n C[n]$.

How in God's name is $\exists n D[n]$ equivalent to $\forall n C[n] \rightarrow \forall n C[n]$?

Answer 1

$$\exists n.(C[n]\to\forall n.C[n])$$ $$\exists n.(C[n]\to\forall m.C[m])$$ $$\exists n.(\neg C[n] \lor \forall m.C[m])$$ $$(\exists n.\neg C[n]) \lor (\exists n.\forall m.C[m])$$ $$(\neg\forall n.C[n]) \lor (\forall m.C[m])$$ $$(\forall n.C[n]) \to (\forall m.C[m])$$ $$(\forall n.C[n]) \to (\forall n.C[n])$$ because $(A\to B)\leftrightarrow (\neg A\lor B)$ and $A\leftrightarrow \exists x.A$ when $A$ does not contain $x$.