Prove that: $\vdash \forall x(\forall y\alpha)\to \forall y(\forall x \alpha)$ How does one prove that

$$\vdash \forall x(\forall y\alpha)\to \forall y(\forall x \alpha)$$

in first order logic?
I have tried using the specialization and generalization rules on various wffs but they don't lead me to anything concrete.
 A: If we have a formula like $\forall x \forall y\ \alpha$, where $\alpha$ is another arbitrary formula, then we can exchange the order of the quantifiers without changing its semantics. Note, however, that this would NOT be possible if the quantifiers were different, e.g. $\forall x \exists y$.
Now why can we do this? Well, if we have a look at how the semantics of classical first-order logic are defined, then this becomes pretty obvious. Let's suppose we wish to evaluate the truth value of the formula for some signature $\Sigma$ over the domain $\mathcal{U}$ and a variable assignment $\gamma$. Furthermore, let's call the truth evaluation function $I$. With this we have
$$I_{\Sigma, \gamma} ( \forall x \forall y\ \alpha ) = \mathbf{T}$$
$$\iff I_{\Sigma, \gamma \cup \{ x \gets c \}} ( \forall y\ \alpha ) = \mathbf{T} \text{ for each $c \in \mathcal{U}$}$$
$$\iff I_{\Sigma, \gamma \cup \{ x \gets c, y \gets d \}} ( \alpha ) = \mathbf{T} \text{ for each $c , d \in \mathcal{U}$.}$$
Obviously, it makes no difference in which order these two quantifiers occur.
Therefore we observe that
$$
\forall x \forall y\ \alpha \to \forall y \forall x\ \alpha
\equiv \forall x \forall y\ \alpha \to \forall x \forall y\ \alpha
\equiv
$$
$$
\equiv \neg \forall x \forall y\ \alpha \lor \forall x \forall y\ \alpha
\equiv \top
\text{,}
$$
thus the formula is valid.
A: 
I have tried using the specialization and generalization rules on various wffs but they don't lead me to anything concrete.

They should.
Just assume $\forall x~(\forall y~\alpha)$, instantiate using fresh arbitrary variables, and generalise in reverse order to derive $\forall y~(\forall x~\alpha)~$, under that assumption.
Now you may deduce $(\forall x~(\forall y~\alpha))\to(\forall y~(\forall x~\alpha))$.
$\blacksquare$
