Theorem 1.2.9 (Church-Rosser for lambda(->)). Assuming that:

  • Γ⊩M:σ

  • M↠βN1

  • M↠βN2

Then there is a λ-term L such that N1↠βL, N2↠βL, and Γ⊩L:σ.