# Lemma relating to alpha equivalence of lambda terms

From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers:

Lemma 1.7.1 Let $$M_{1} =_{\alpha} N_{1}$$ and $$M_{2} =_{\alpha} N_{2}$$. Then also:

(1) $$M_{1}N_{1} =_{\alpha} M_{2}N_{2}$$,

(2) $$\lambda x . M_{1} =_{\alpha} \lambda x . M_{2}$$,

(3) $$M_{1}[x := N_{1}] =_{\alpha} M_{2}[x := N_{2}]$$.

Why does this hold? There does not seem to be a stated connection between $$M_{1}$$ and $$M_{2}$$ or $$N_{1}$$ and $$N_{2}$$.

• It is just a typo. The hypothesis of lemma 1.7.1 should be $M_1 =_\alpha M_2$ and $N_1 =_\alpha N_2$. – Taroccoesbrocco Dec 21 '18 at 3:56
• I see. Thank you! – user695931 Dec 21 '18 at 4:04