Why is $\lambda x.\lambda y. x y$ $\alpha$-equivalent to $\lambda x. \lambda y. yx$?

Question

Why is $\lambda x.\lambda y. x y$ $\alpha$-equivalent to $\lambda x. \lambda y. yx$? Can we prove it by strict steps based on the definition of $\alpha$-equivalence in the $\lambda$-calculus?

Answer 1

$\lambda x. \lambda y.x(y)$ is NOT $\alpha$-equivalent to $\lambda x.\lambda y.y(x)$.

Indeed, suppose for the sake of contradiction that $\lambda x. \lambda y.x(y)$ is $\alpha$-equivalent to $\lambda x.\lambda y.y(x)$. Then, \begin{align} \lambda x. \lambda y.x(y) &=_\beta \lambda x.\lambda y.y(x) &\text{because $\beta$-conversion contains $\alpha$-equivalence} \\ (\lambda x. \lambda y.x(y))z_1z_2 &=_\beta (\lambda x.\lambda y.y(x))z_1z_2 &\text{by contextual closure} \\ z_1z_2 &=_\beta z_2z_1 &\text{by $\beta$-conversion} \end{align} But $z_1z_2$ and $z_2z_1$ are normal and syntactically different terms, so $z_1z_2 \neq_\beta z_2z_1$. Contradiction.