For several applications, for example for the problem of finding all possible inhabitants of a given type, we will need the weak normalization theorem, which states that all typable terms do have a βη-nf (normal form). The result is valid for all versions of and a fortiori for the subsystem . The proof is due to Turing and was published posthumously in Gandy (1980). In fact all typable terms in these systems are βη strongly normalizing, which means that all βη-reductions are terminating. This fact requires more work ...