Chapitre

1°. Tout type déduit du schème est un type attaché à la proposition.

Pour obtenir un type déduit du schème, on peut en effet enlever une variable dominante du schème; du nouveau schème ainsi obtenu, on enlève une variable dominante dans ce nouveau schème qu’on met à droite de la précédente; et ainsi de suite jusqu’à ce qu’on ait épuisé toute les variables. Il résulte alors de la remarque 1.43 et du Lemme 1 (1.12) que l’on peut enlever dans cet ordre toutes les variables de la proposition considérée; et donc que cet ordre donne un type attaché à la proposition.

2 Tout type attaché à la proposition est un type déduit du schème.

Il suffit pour le voir de remarquer que si dans une proposition x est supérieur à y, alors y ne peut dominer x, et de se rappeler la propriété caractéristique des types déduits du schème (1.42).