Solution
= Solution
Choose distinct fresh variables $a,b$. Instantiate the outer <universal quantifier> first, then the inner one; generalize them in the opposite order.
``
1. ∀x ∀y P(x,y) premise
2. ∀y P(a,y) ∀E, 1
3. P(a,b) ∀E, 2
4. ∀x P(x,b) ∀I, 3, generalizing a
5. ∀y ∀x P(x,y) ∀I, 4, generalizing b
``
Neither $a$ nor $b$ occurs free in the sole undischarged premise. Thus both <universal introduction> steps satisfy the <eigenvariable condition>.