Theorem 1.2.14 (Weak normalisation for lambda(->)). Assuming that:

Then there is a finite reduction path

M : = M_{0} \to_{β} M_{1} \to_{β} M_{2} \to_{β} \dots \to_{β} M_{n}

, where

M_{n}

is in

β