Theorem 1.2.15 (Strong Normalisation for lambda(->)). Assuming that:

  • Γ⊩M:σ

Then there is no infinite reduction sequence M→βM1→β⋯.