. Proof, Assume that T = ñ T 1 U 1 ð = U. Then, T ? = ñ T 1 ? and U? = ñ U 1 ? from properties of rewriting

. Proof, Straightforward induction on the denition of t 1 u 1 , where t 1 and u 1 are s.t. t = ñ t 1

. Proof, The proof is identical to the one of CAC, using classes preservation of

?. If, T , t ? Ñ t 1 , ? ( ? and t? P WN, then t ?,? t 1 ?,? Proof. Following the proof of Lemma 65 of

. Proof, Following the proof of Lemmas 63 and 68 of

. Proof and . Let, Since ? ( ? and the identity substitution ? is adapted to ?, t P S T ?,? . Now, either T or ? , T : s for some s P S. If T , then S J SN. If ? , T : s, then T P R s and R s „ SN by (R1)

. Proof, Straightforward induction on the denition of ? (resp. ? )

B. Barras, Auto-Validation d'un système de preuves avec familles inductives, 1999.

G. Barthe, The relevance of proof-irrelevance, Lecture Notes in Computer Science, vol.1443, p.755768, 1998.
DOI : 10.1007/BFb0055099

F. Blanqui, Type Theory and Rewriting, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00105525

F. Blanqui, Denitions by rewriting in the calculus of constructions, Mathematical Structures in Computer Science, vol.15, issue.1, p.3792, 2005.

F. Blanqui, Inductive Types in the Calculus of Algebraic Constructions, Fundam. In form, vol.65, issue.12, p.6186, 2005.
DOI : 10.1007/3-540-44904-3_4
URL : https://hal.archives-ouvertes.fr/inria-00105617

F. Blanqui, J. Jouannaud, and P. Strub, Building Decision Procedures in the Calculus of Inductive Constructions, Lecture Notes in Computer Science, vol.4646, p.328342, 2007.
DOI : 10.1007/978-3-540-74915-8_26
URL : https://hal.archives-ouvertes.fr/inria-00160586

A. Bouhoula, J. Jouannaud, and J. Meseguer, Specication and proof in member ship equational logic, Theor. Comput. Sci, vol.236, issue.12, p.35132, 2000.

A. Church, A simple theory of types, Journal of Symbolic Logic, vol.5, p.5668, 1940.

R. Constable, S. Allen, M. Bromley, R. Cleaveland, J. Cremer et al., Implementing mathematics with the Nuprl proof development system, 1986.

T. Coquand, An analysis of girard's paradox, 1986.

T. Coquand, An algorithm for testing conversion in type theory, 1991.
DOI : 10.1017/CBO9780511569807.011

T. Coquand and G. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, p.95120, 1988.
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024

T. Coquand and G. P. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, p.95120, 1988.
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024

T. Coquand and C. Paulin, Inductively dened types, COLOG-88: Proceedings of the international conference on Computer logic, p.5066, 1990.
DOI : 10.1007/3-540-52335-9_47

H. Curry and R. Feys, Combinatory Logic I. Studies in Logic and the Foundations of Mathematics, 1958.

N. De-bruijn, The mathematical language AUTOMATH, its usage, and some of its extensions, Proc. of Symp. on Automatic Demonstration, p.2961, 1970.

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, J. Autom. Reason ing, vol.31, issue.1, p.3372, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01199506

G. Dowek and B. Werner, Proof normalization modulo, Lecture Notes in Computer Science, vol.1657, p.6277, 1998.
DOI : 10.1007/3-540-48167-2_5
URL : https://hal.archives-ouvertes.fr/inria-00073143

G. Gentzen, Untersuchungen über das logisches schlieÿen, Mathematische Zeitschrift, vol.1, p.176210, 1935.

H. Geuvers and M. Nederhof, Modular proof of strong normalization for the calculus of constructions, J. Funct. Program, vol.1, issue.2, p.155189, 1991.

E. Gimenez, Structural recursive denitions in type theory, Automata, Languages and Programming, p.397408, 1998.

J. Girard, Une extension de l'interprétation de gödel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types, Proc. of the 2nd Scandinavian Logic Symposium, 1971.

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, 1988.

G. Gonthier, The four color theorem in coq, TYPES 2004 International Workshop, 2004.

M. Gordon and T. Melham, Introduction to HOL: A theorem proving envi ronment for higher order logic, 1993.

W. A. Howard, The formulae-as-types notion of construction, To H. B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism, 1969.

J. Jouannaud and M. Okada, A computation model for executable higher-order algebraic specication languages, LICS, p.350361, 1991.

Z. Luo, ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, p.386395, 1989.
DOI : 10.1109/LICS.1989.39193

P. Martin-löf, Haupsatz for the intuitionistic theory of iterated inductive denitions, Proc. of the 2nd Scandinavian Logic Symposium of Studies in Logic and the Foundations of Mathematics, 1971.

P. Martin-löf, Intuitionistic type theory, Bibliopolis, 1984.

R. Milner, Implementation and applications of Scott's logic for computable functions, ACM sigplan notices, vol.7, issue.1, p.16, 1972.

N. Oury, Extensionality in the Calculus of Constructions, Lecture Notes in Computer Science, vol.3603, p.278293, 2005.
DOI : 10.1007/11541868_18

S. Owre, J. Rushby, and N. Shankar, PVS: A prototype verification system, Proc. 11th Int. Conf. on Automated Deduction, p.748752, 1992.
DOI : 10.1007/3-540-55602-8_217

L. Paulson, Experience with Isabelle : A generic theorem prover, 1988.

L. Paulson, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol.828, 1994.
DOI : 10.1007/BFb0030541

D. Prawitz, Natural Deduction: a Proof-Theoretical Study, volume 3 of Stockholm Studies in Philosophy, 1965.

P. Severi and E. Poll, Pure type systems with denitions, LFCS, p.316328, 1994.
DOI : 10.1007/3-540-58140-5_30
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.1076

N. Shankar, Little engines of proof, FME 2002: Formal Methods Getting IT Right, p.120, 2002.

R. E. Shostak, Deciding combinations of theories, J. ACM, vol.31, issue.1, p.112, 1984.

V. Tannen, Combining algebra and higher-order types, LICS, p.8290, 1988.

V. Tannen and J. H. Gallier, Polymorphic rewriting conserves algebraic strong nor malization and conuence, Lecture Notes in Computer Science, vol.372, p.137150, 1989.

V. Tannen and J. H. Gallier, Polymorphic rewriting conserves algebraic conuence, Inf. Comput, vol.114, issue.1, p.129, 1994.

A. Trybulec, The Mizar-QC/6000 logic information language, Association for Literary and Linguistic Computing Bulletin, p.136140, 1978.

B. Werner, Une théorie des Constructions Inductives, 1994.