2.3 Normalisation
On dit qu'un terme M est typable (avec les types simples) s'il existe un
contexte C et un type s tels que C|- M:s.
Voici le théorème :
Théorème 5 Tout terme typable (avec les types simples) est fortement normalisable.
On n'en donnera pas la preuve.