induction on $A$.

Let $\varphi$ a special $\m$-variable. A term $M \in {\cal M}''$ is translated into a $\l\m$-term $M^{\circ}$ as follows:

-   $\{x\}^{\circ}= x$

-   $\{\l x. M\}^{\circ}= \l x. M^{\circ}$

-   $\{(M \; N)\}^{\circ}= (M^{\circ} \; N^{\circ})$

-   $\{\m \a. M\}^{\circ} = \m \a.  M^{\circ}$

-   $\{(\a \; M)\}^{\circ} = (\a \; M^{\circ})$

-   $\{\<M ,N\>\}^{\circ}= \l x. (x \; M^{\circ} \; N^{\circ})$

-   $\{M \pi_i\}^{\circ}= \m \a. (\vp \; (M^{\circ} \; \l x_1.\l x_2.
      \m \g. (\a \; x_i)))$ where $\g$ is a fresh variable

-   $\{M \; [x_1.N_1 , x_2.N_2]\}^{\circ}= \m \a. (\vp \; (M^{\circ}
      \; \l x_1. \m \g. (\a \; N_1^{\circ}) \; \l x_2. \m \g. (\a \;
      N_2^{\circ})))$ where $\g$ is a fresh variable

-   $\{\o_i M\}^{\circ}= \l x_1. \l x_2. (x_i \; M^{\circ})$

[**Remarks**]{}

-   The introduction of the free variable $\vp$ in the definition of $\{M \; [x_1.N_1 , x_2.N_2]\}^{\circ}$ and $\{M \pi_i\}^{\circ}$ is not necessary for lemma \[coding2\]. The reason of this introduction is that, otherwise, to simulate the reductions of the $\l\m^{\f\et\ou}$-calculus we would have to introduce new reductions rules for the $\l\m$-calculus and thus to prove $SN$ of this extension whereas, using $\vp$, the simulation is done with 