the usual rules of the $\l\m$-calculus.

-   There is another way of coding $\et$ and $\ou$ by using intuitionistic second order logic.

    -   $\{A_1 \et A_2\}^{\circ}= \forall X ((A_1^{\circ} \f
          (A_2^{\circ} \f X)) \f X)$

    -   $\{A_1 \ou A_2\}^{\circ}= \forall X ((A_1^{\circ} \f X) \f
          ((A_2^{\circ} \f X) \f X))$

    The translation of $\{\<M ,N\>\}^{\circ}$ and $\{\o_i
    M\}^{\circ}$ are the same but the translation of $\{M
    \pi_i\}^{\circ}$ will be $(M^{\circ} \; \l x_1.\l x_2.x_i)$ and the one of $\{M \; [x_1.N_1 , x_2.N_2]\}^{\circ}$ would be $
    (M^{\circ} \; \l x_1.N_1^{\circ} \; \l x_2.N_2^{\circ})$. But it is easily checked that the permutative conversions are not correctly simulated by this translation whereas, in our translation, they are.

-   Finally note that, as given in definition \[def\_red\], the reduction rules for the $\l\m^{\f\et\ou}$-calculus do not include $\tr_{\r}$ and $\tr_{\th}$. We could have added them and the given translation would have worked in a similar way. We decided not to do so (although these rules were already considered by Parigot) because they, usually, are not included neither in the $\l\m$-calculus nor in the $\l\m^{\f\et\ou}$-calculus. Moreover some of the lemma given below would need a bit more complex statement.

1.  $\{M[x:=N]\}^{\circ} = M^{\circ}[x:=N^{\circ}]$.

2.  $\{M[(\a 