If $M \tr_{\r}^* P$ and $M \tr_{\b\m\r\th}^* Q$, then $P
\tr_{\b\m\r\th}^* N$, $Q \tr_{\r}^* N$ for some $N$ and $lg_{\b\m}(P \tr_{\b\m\r\th}^* N) = lg_{\b\m}(M \tr_{\b\m\r\th}^*
Q)$.

By induction on $lg_{\b\m}(M \tr_{\b\m\r\th}^* Q)$. If $M
\tr_{\b\m\r\th}^* M_1 \tr_{\b\m} M_2 \tr_{\r\th}^* Q$, then, by induction hypothesis, $P \tr_{\b\m\r\th}^* N_1$, $M_1 \tr_{\r}^*
N_1$ and $lg_{\b\m}(P \tr_{\b\m\r\th}^* N_1) = lg_{\b\m}(M \tr^*
M_1)$. By (3) of lemma \[new\], $N_1 \tr_{\b\m} N_2$ and $M_2
\tr_{\r}^* N_2$ for some $N_2$. And finally, by (2) of lemma \[new\], $N_2 \tr_{\r\th}^* N$ and $Q \tr_{\r}^* N$ for some $N$. Thus $P \tr_{\b\m\r\th}^* N$, $Q \tr_{\r}^* N$ and $lg_{\b\m}(P \tr_{\b\m\r\th}^* N) = lg_{\b\m}(M \tr_{\b\m\r\th}^*
Q)$.

A translation of the $\l\m^{\f\et\ou}$-calculus into the $\l\m$-calculus {#6}
========================================================================

We code $\et$ and $\ou$ by their usual equivalent (using $\f$ and $\bot$) in classical logic.

We define the translation $A^{\circ} \in \cal{T}$ of a type $A \in \cal{T}'$ by induction on $A$ as follows.

-   $\{A\}^{\circ}= A$ for $A \in {\cal A}\cup \{\bot\}$

-   $\{A_1 \f A_2\}^{\circ}= A_1^{\circ} \f A_2^{\circ}$

-   $\{A_1 \et A_2\}^{\circ}= \neg (A_1^{\circ} \f (A_2^{\circ} \f
      \bot))$

-   $\{A_1 \ou A_2\}^{\circ}= \neg A_1^{\circ} \f (\neg A_2^{\circ} \f
      \bot)$

For every $A \in {\cal T}'$, $A^{\circ}$ is classically equivalent to $A$.

By 