. Conversely, Assume without loss of generality that x does not appear in ?, nor in ?, ?, ?. By hypothesis (? ??xA) ? ?xA ? . If ? ??xA has a neutral cut-free proof then so does the sequent ? (?t/x)?A) Since ?(t/x)A = (?t/x)?A, we have (? ?((t/x)A)) ? A ?+(t ? /x) , which is equal to (t/x)A ? by Proposition 3.6. Otherwise, Definition 3.3 ensures that for any d, including t ?, A)) ? (t/x)A ?

?. So, ? We first show that [?xA] is an upper bound of the set { Consider some term t, and a context ? ? Let ? be an assignment, ? be a substitution and ? a ?-adapted context. Assume without loss of generality that x does not appear in ? nor in ? Since ?(t/x)A = (?t/x)?A, we have by hypothesis (? (?t/x)(?A)) ? (t/x)A ? , which is equal to A ?+C i ] be an upper bound of { Let ? be an assignment and ? be a substitution, let ? be ?-adapted and assume, without loss of generality, We can choose c = [C], since we need the intersection of the upper bounds

?. Assume, Then, since ?A is A-adapted, we have (?A ?C) ? C ? In particular, by Proposition 3.5, this sequent has a cut-free proof. Since x does not appear in C nor in ?, we can apply an ?-elimination rule between a proof of this sequent and the neutral cut-free proof of ? ?x?A, yielding a neutral cut-free proof of ? ?C. Hence (? ?C) ? C ? . Otherwise, by Definition 3.3, ? ?x?A is such that for some term t and element d, (? ? A) ? A ? , calling ? = ?

P. B. Andrews, Resolution in type theory, The Journal of Symbolic Logic, vol.34, issue.03, pp.414-432, 1971.

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

D. Marco, M. , and J. Lipton, Completeness and cut elimination in Church's intuitionistic theory of types, Journal of Logic and Computation, vol.15, pp.821-854, 2005.

G. Dowek, Truth Values Algebras and Proof Normalization, TYPES, pp.110-124, 2006.

G. Dowek, T. Hardin, and C. Kirchner, Hol-lambda-sigma: an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, pp.1-25, 2001.

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.

G. Dowek and O. Hermant, A Simple Proof That Super-Consistency Implies Cut Elimination, RTA, pp.93-106, 2007.

G. Dowek and B. Werner, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116

J. Girard, Une extension de l'interprétation de Gödeì a l'analyse et son applicationàapplication`applicationà l'´ elimination des coupures dans l'analyse et la théorie des types, Proceedings of the Second Scandinavian Logic Symposium of Studies in Logic and the Foundations of Mathematics, pp.63-92, 1970.

O. Hermant and J. Lipton, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, CSL, pp.169-183, 2008.

O. Hermant and J. Lipton, Completeness and Cut-elimination in the Intuitionistic Theory of Types--Part 2, Journal of Logic and Computation, vol.20, issue.2, pp.597-602, 2010.

M. Okada, A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science, vol.281, issue.1-2, pp.471-498, 2002.

D. Prawitz, Hauptsatz for higher order logic, The Journal of Symbolic Logic, vol.25, issue.03, pp.452-457, 1968.

K. Schütte, Syntactical and semantical properties of simple type theory, The Journal of Symbolic Logic, vol.15, issue.04, pp.305-326, 1960.
DOI : 10.1007/BF01969991

W. W. Tait, A nonconstructive proof of Gentzen's Hauptsatz for second order predicate logic, Bulletin of the American Mathematical Society, vol.72, issue.6, pp.980-983, 1966.

M. Takahashi, A proof of cut-elimination theorem in simple type-theory, Journal of the Mathematical Society of Japan, vol.19, issue.4, pp.399-410, 1967.