\; N):= (\a \; (N \; \ep))]\}^{\circ} = M^{\circ}[(\a \;
      N^{\circ}):= (\a \; \{(N \; \ep)\}^{\circ})]$.

By induction on $M$.

\[coding2\] If $\G \v_{{\cal S}^{\f\et\ou}} M : A$, then $\G^{\circ} \v_{{\cal
S}^{\m}} M^{\circ} : A^{\circ}$ where $\G^{\circ}$ is obtained from $\G$ by replacing all the types by their translations and by declaring $ \vp$ of type $ \neg \bot$.

By induction on a derivation of $\G \v_{{\cal S}^{\f\et\ou}} M : A$.

\[simulation2\] Let $M \in {\cal M}''$. If $M \tr N$, then there is $P \in {\cal M}'$ such that $M^{\circ} \tr_{\b\m\r\th}^* P$, $N^{\circ} \tr_{\r}^*P$ and $lg_{\b\m}(M^{\circ} \tr_{\b\m\r\th}^* P) \geq 1$.

By case analysis. The details are given in the appendix, section \[app\].

\[simulation3\] Let $M \in {\cal M}''$. If $M \tr^* N$, then there is $P\in {\cal M}'$ such that $M^{\circ} \tr_{\b\m\r\th}^* P$, $N^{\circ} \tr_{\r}^* P$ and $lg_{\b\m}(M^{\circ} \tr_{\b\m\r\th}^* P) \geq lg(M \tr^* N)$.

By induction on $lg(M \tr^* N)$. If $M \tr^* L \tr N$, then, by induction hypothesis, there is $Q\in {\cal M}'$ such that $M^{\circ}
\tr_{\b\m\r\th}^* Q$, $L^{\circ} \tr_{\r}^* Q$ and $lg_{\b\m}(M^{\circ} \tr_{\b\m\r\th}^* Q) \geq lg(M \tr^* L)$. By lemma \[simulation2\], there is a $R \in {\cal M}'$ such that $L^{\circ} \tr_{\b\m\r\th}^* R$, $N^{\circ} \tr_{\r}^*R$ and 