if, on types, we allow some equations satisfying natural (and necessary) conditions. Mendler’s result concerned the implicative fragment of intuitionistic logic. By using the previous translation, we extend here this result to full classical logic .

The paper is organized as follows. Section \[2\] gives the various systems for which we prove the strong normalization. Section \[6\] gives the translation of the $\l\m^{\f\et\ou}$-calculus into the $\l\m$-calculus and section \[7\] extends Mendler’s theorem to the $\l\m^{\f\et\ou}$-calculus. For a first reading, sections \[3\], \[4\] and \[rab\] may be skipped. They have been added to have complete proofs of the other results. Section \[3\] contains the proof, by the first author, of the the strong normalization of the simply typed $\l$-calculus. Section \[4\] gives a translation of the $\l\m$-calculus into the $\l$-calculus and section \[rab\] gives some well known properties of the $\l\m$-calculus. Finally, the appendix gives a detailed proof of a lemma that needs a long but easy case analysis.

The systems {#2}
===========

Let ${\cal V}$ and ${\cal W}$ be disjoint sets of variables.

1.  The set of $\l$-terms is defined by the following grammar

    $${\cal M} := {\cal V} \ | \ \l {\cal V}.  {\cal M} \ | \ 