A. Avron, F. Honsell, I. A. Mason, and R. Pollack, Using typed lambda calculus to implement formal systems on a machine, Journal of Automated Reasoning, vol.49, issue.3, pp.309-354, 1992.
DOI : 10.1007/BF00245294

F. [. Avron, M. Honsell, C. Miculan, and . Paravano, Encoding Modal Logics in Logical Frameworks, Studia Logica, vol.60, issue.1, pp.161-208, 1998.
DOI : 10.1023/A:1005060022386

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure Pattern Type Systems, Proc. of POPL, pp.250-261, 2003.

H. Barendregt and H. Geuvers, Proof-Assistants Using Dependent Type Systems, Handbook of Automated Reasoning, pp.1149-1238, 2001.
DOI : 10.1016/B978-044450813-3/50020-5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7813

M. Cresswell and G. Hughes, A companion to Modal Logic, 1984.

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

R. Constable and D. Howe, NuPRL as a General Logic, Logic and Computation, 1990.

]. H. Ckl01a, C. Cirstea, L. Kirchner, and . Liquori, Matching Power, Proc. of RTA, pp.77-92, 2001.

]. H. Ckl01b, C. Cirstea, L. Kirchner, and . Liquori, The Rho Cube, Proc. of FOSSACS, pp.166-180, 2001.

R. L. Constable, Implementing Mathematics with the Nuprl Proof Development System, 1986.

. Coq, The Coq Home Page, 2006.

T. Coquand, R. Pollack, and M. Takeyama, A Logical Framework with Dependently Typed Records, Prof. of TLCA, pp.105-119, 2003.
DOI : 10.1007/3-540-44904-3_8

N. G. De-bruijn, A Survey of the Project Automath, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp.589-606, 1980.
DOI : 10.1016/S0049-237X(08)70203-9

J. Despeyroux, A Higher-Order Specification of the ??-Calculus, Proc. of IFIP TCS, pp.425-439, 2000.
DOI : 10.1007/3-540-44929-9_30

D. J. Dougherty, Adding algebraic rewriting to the untyped lambda calculus, Information and Computation, vol.101, issue.2, pp.251-267, 1992.
DOI : 10.1016/0890-5401(92)90064-M

S. Feferman, Finitary inductively presented logics, Proc. of Logic Colloquium, 1988.
DOI : 10.1016/S0049-237X(08)70270-2

F. [. Harper, G. Honsell, and . Plotkin, A Framework for Defining Logics Preliminary version in proc, Journal of the ACM, vol.4087, issue.1, pp.143-184, 1993.

M. [. Jouannaud and . Okada, Executable Higher-Order Algebraic Specification Languages, Proc. of LICS, pp.350-361, 1991.

R. [. Kamareddine, R. Bloo, and . Nederpelt, On ??-conversion in the ??-cube and the combination with abbreviations, Annals of Pure and Applied Logic, vol.97, issue.1-3, pp.1-327, 1999.
DOI : 10.1016/S0168-0072(98)00019-0

]. J. Kvovr93, V. Klop, F. Van-oostrom, and . Van-raamsdonk, Combinatory Reduction Systems: Introduction and Survey, Theoretical Computer Science, vol.121, pp.279-308, 1993.

L. Liquori, F. Honsell, and R. Redamalla, A Language for Verification and Manipulation of Web Documents, Proc. of WWV, pp.127-137, 2005.
DOI : 10.1016/j.entcs.2005.12.046
URL : https://hal.archives-ouvertes.fr/hal-01148880

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

]. P. Mar84 and . Martin-löf, Intuitionistic Type Theory, volume 1 of Studies in Proof Theory, Bibliopolis, 1984.

. [. Martin-lof, Truth of a Proposition, Evidence of a Judgement, Validity of a Proof. Lecture given at the Workshop Theories of Meaning, 1985.

]. R. Nge94, J. H. Nederpelt, and R. Geuvers, Selected Papers on Automath, 1994.

M. Okada, Strong normalizability for the combined system of the typed lmbda calculus and an arbitrary convergent term rewrite system, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation , ISSAC '89, pp.357-363, 1989.
DOI : 10.1145/74540.74582

]. V. Oos94 and . Van-oostrom, Confluence for Abstract and Higher-Order Rewriting, 1994.

L. Paulson, Interactive Theorem Proving with Cambridge LCF, 1985.

F. Pfenning, Logical Frameworks, Handbook of Automated Reasoning, volume II, pp.1063-1147, 2001.
DOI : 10.1016/B978-044450813-3/50019-9

]. G. Plo75 and . Plotkin, Call by Name, Call by Value and the ?-calculus, Theoretical Computer Science, vol.1, pp.125-159, 1975.

C. [. Pfenning and . Schurmann, System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, Proc. of CADE, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

M. Takahashi, Parallel reductions in ??-calculus, Journal of Symbolic Computation, vol.7, issue.2, pp.113-123, 1989.
DOI : 10.1016/S0747-7171(89)80045-8

V. Van-oostrom, Lambda Calculus with Patterns, 1990.

B. Wack, Typage et déduction dans le calcul de réécriture, 2005.

F. Comp, O. , Q. Sn, and M. , F satisfies condition (c3) of Definition 3.22. Thus, for provingx]? F , it is sufficient to prove that CoDom(? SN F , since by the Subderivation Property 3.14, for each family A ? CoDom(?), there exists a smaller derivation of ? ? A : K; hence, we can apply the induction hypothesis to this latter derivation, Now, since Q ? B F , then, by Lemma 3.25, we get Q ? SN O . Moreover, CoDom by induction hypothesis, noticing that Dom(?) = Dom(?)

@. Proof, F. Sn-o-q-?, and . Sn-o, Moreover, by Lemma 3.25, we get A Thus, since SN O is closed under (c4), using the Subderivation Property 3, p.we get (?P :?