Prerequisites
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$.
Question
Now, probably an easy one:
Prove that $$\lambda x .x =_\beta x$$ doesn't hold.
Comments
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.
The Church-Rosser property is all you need: $\lambda x.x$ and $x$ are both $\rightarrow_{\beta}$-normal forms so they can only be $\rightarrow_{\beta}$-equivalent if they are $\alpha$-equivalent, which they are not.
To explain this in more detail, let me write $a \rightarrow b$ to mean that $b$ can be obtained from $a$ by repeated $\beta$-reductions. The Church-Rosser property says that if $a \rightarrow b$ and $a \rightarrow c$ then there is a term $d$ such that $b \rightarrow d$ and $c \rightarrow d$. If $\lambda x.x$ and $x$ were $\rightarrow_{\beta}$-equivalent, then there would be a sequence of terms $t_1, \ldots, t_n$ with $t_1 \equiv \lambda x.x$ and $t_n \equiv x$ such that for each $i$, $1 \le i < m$ either $t_i\rightarrow t_{i+1}$ or $t_{i+1}\rightarrow t_i$. Church-Rosser lets you transform any triple of the form $t_{i-1} \leftarrow t_{i} \rightarrow t_{i+1}$ in this sequence into a triple of the form $t_{i-1} \rightarrow t_{i}' \leftarrow t_{i+1}$. Repeatedly applying this transformation will result in a sequence $t_1', \dots, t_n'$ with $t_1' \equiv \lambda x.x$ and $t_n' \equiv x$, such that $t_1' \rightarrow t_2'$ and $t_n' \rightarrow t_{n-1}'$. But $t_1'$ and $t_n'$ are both $\rightarrow_{\beta}$-normal forms, so this is impossible, unless $t_1' = t_2' = \ldots = t_{n-1}' = t_n'$, which is not the case if $t_1' \equiv \lambda x.x$ and $t_n' \equiv x$.