Le Calcul des Constructions Algébriques (CAC) est une extension du Calcul des Constructions avec des symboles de fonction et de prédicats définis par des règles de récriture d'ordre supérieur. Les types y sont identifiés modulo béta-réduction et récriture. Par ailleurs, le Calcul des Constructions Inductives (CIC), à la base de l'assistant à la démonstration Coq, est une extension du Calcul des Constructions avec des types inductifs et leurs récurseurs associés définis par les règles dites de iota-réduction. Les fonctions et les prédicats doivent être définis par récurrence à l'aide des récurseurs, et les types sont identifiés modulo béta et iota-réduction. Étant donné que la iota-réduction est un cas particulier de récriture d'ordre supérieur, la question se pose de savoir si CIC peut être vu comme un CAC et si les conditions de terminaison établies pour CAC sont vérifiées par CIC. Or il apparaît que la méthode employée dans ma thèse pour montrer la terminaison de CAC ne permet pas de capturer tous les types inductifs de CIC. Dans cet exposé, je présente une nouvelle méthode qui permet de capturer tous les types inductifs de CIC et bien plus, des types inductifs-récursifs par exemple.