Consider the $\lambda$-calculus where terms are equivalence classes over the $\alpha$-equality.
We define $\to_\beta$-reduction in the usual way, i.e. the least congruent relation on $\lambda$-terms (hence congruent with application and abstraction) satisfying
$$(\lambda x. M) N \to_\beta M[x := N]$$
Following this, $=_\beta$ is defined as the least equivalence relation containing $\to_\beta$.
Now, probably an easy one:
Prove that $$\lambda x .x =_\beta x$$ doesn't hold.
It is clear to me that the above equation does not hold. On both sides are normal forms which differ. I can even prove it using a lot of machinery: Church-Rosser, parallel reduction relation and an order in beta-reduction sequences. But it seems as if this should be an easy one and I'm just overlooking something. Insofar I'm looking for ideas for a formal proof.
Exercise is based on one from the book "Lectures on the Curry-Howard Isomorphism" by Sørensen and Urzyczyn.