})<\eta_{\b}(M)$ and the result follows from the induction hypothesis.

-   $M=(x\;P\;\overrightarrow{O})$. By the induction hypothesis, $P_{1}=P[x:=N]$ and $\overrightarrow{O_{1}}=\overrightarrow{O}[x:=N]$ are in $SN_{\b}$. By lemma \[a\] it is enough to show that if $N
    \tr_{\b}^*\l y.N_{1}$ then $M_{1}=(N_{1}[y:=P_{1}]\;
    \overrightarrow{O_{1}}) \in SN_{\b}$. By the induction hypothesis (since $ type(P_{1})<type(N)$) $N_{1}[y:=P_{1}] \in SN_{\b}$ and thus, by the induction hypothesis (since $M_{1}=(z\;\overrightarrow{O_{1\;}})\;[z:=N_{1}[y:=P_{1}]]$ and $type(N_{1})<type(N)$) $M_{1} \in SN_{\b}$.

\[sn\_rd\] The simply typed $\l$-calculus is strongly normalizing.

By induction on $M$. The cases $M=x$ or $ M=\lambda x.P$ are trivial. If $M=(N \ P)=(z\;P)[z:=N]$ this follows from lemma \[b\] and the induction hypothesis.

A translation of the $\l\m$-calculus into the $\l$-calculus {#4}
===========================================================

We give here a translation of the simply typed $\l\m$-calculus into the simply typed $\l$-calculus. This translation is a simplified version of Parigot’s translation in [@Par2]. His translation uses both a translation of types (by replacing each atomic formula $A$ by $\neg\neg A$) and a translation of terms. But it is known that, in the implicative fragment of propositional logic, it is enough to add $\neg\neg$ in front of the rightmost variable. The translation we have chosen consists in decomposing the formulas (by using the terms $T_A$) until the rightmost variable is found and 