(as pointed out by Matthes in a private communication) it also contains some errors.

[*Semantical proofs*]{}. K. Saber and the second author gave in [@NaSa] a semantical proof of this result by using the notion of saturated sets. This proof is a generalization of Parigot’s strong normalization result of the $\lambda\mu$-calculus with the types of Girard’s system ${\cal F}$ by using reducibility candidates. This proof uses the technical lemma of [@DaNo2] concerning commutative reductions. In [@Mat2] and [@Tats], R. Matthes and Tastuta give another semantical proofs by using a (more complex) concept of saturated sets.

This paper presents a new proof of the strong normalization of the simply typed $\l\m^{\f\et\ou}$-calculus. This proof is formalizable in Peano first order arithmetic and does not need any complex lemma. It is obtained by giving a translation of this calculus into the $\l\m$-calculus. The coding of $\et$ and $\ou$ in classical logic is the usual one but, as far as we know, the fact that this coding behaves correctly with the computation, via the Curry-Howard correspondence, has never been analyzed. This proof is much simpler than the existing ones[^1].

It also presents a new result. Mendler [@Mend2] has shown that strong normalization is preserved 