$\G^{\diamond}$ is obtained from $\G$ by replacing $\a : \neg B$ by ${x}_{\a} : \neg B$.

By induction on the typing $\G \v_{{\cal S}^{\m}} M : A$. Use lemma \[tran\].

\[SN\_M\] The simply typed $\l\m$-calculus is strongly normalizing for $\tr_{\b\m}$.

A consequence of lemmas \[sn1-&gt;sn2\], \[coding1\] and theorem \[sn\_rd\].

Some classical results on the $\l\m$-calculus {#rab}
=============================================

The translation given in the next section needs the addition, to the $\l\m$-calculus, of the following reductions rules.

$(\b \; \mu \a. M) \tr_{\r} M[\a := \b]$

$\mu \a. (\a \; M) \tr_{\th} M$ if $\a \not \in Fv(M)$

We will need some classical results about these new rules. For the paper to remain self-contained, we also have added their proofs. The reader who already knows these results or is only interested by the results of the next section may skip this part.

Adding $\tr_{\r\th}$ does not change $SN$
-----------------------------------------

\[retardemant\] Let $M \in {\cal M}'$ be such that $M \in SN_{\b\m}$. Then $M \in
SN_{\b\m\r\th}$.

This follows from the fact that $\tr_{\r\th}$ can be postponed (theorem \[ch1:pprt\] below) and that $\tr_{\r\th}$ is strongly normalizing (lemma \[SNrth\] below).

\[SNrth\] The reduction $\tr_{\r\th}$ is strongly normalizing.

The reduction $\tr_{\r\th}$ decreases the size.

\[ch1:pprt\] Let 