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}$.

  • 1
    $\begingroup$ 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$. $\endgroup$ – Taroccoesbrocco Dec 21 '18 at 3:56
  • $\begingroup$ I see. Thank you! $\endgroup$ – user695931 Dec 21 '18 at 4:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.