Je présenterai un nouveau système de type au pouvoir expressif
étonnant et qui permet notemment d'extraire des combinateurs de points
fixes de preuves ! On présentera entre autre une dérivation de la règle
du point fixe de TTR (n'utilisant pas les ordinaux, ce que je ne savais
pas faire avec la sémantique).
Note: ST veut dire sous-typage.