rules (where $\G$ now is a $\l\m$-context) the following rules.

    $\F{\G , \a : \neg A \v M : A} {\G , \a : \neg A\v (\a \; M) :
    \bot} \bot_i$ $\F{\G , \a : \neg A \v M : \bot} {\G
    \v \mu \a.M : A} \bot_e$

3.  The simply typed $\l\m^{\f\et\ou}$-calculus (denoted ${\cal
    S}^{\f\et\ou}$) is defined by adding to the previous rules (where $\G$ now is a $\l\m^{\f\et\ou}$-context) the following rules.

    $\F{\G \v M : A_1 \quad \G \v N : A_2} {\G \v \< M,N \>
    : A_1 \et A_2} \, \et_i$ $\F{\G \v M : A_1 \et A_2}
    {\G \v  (M \; \pi_i): A_i } \, \et_e$

    $\F{\G \v M :
    A_j} {\G \v \o_j M : A_1 \ou A_2} \, \ou_i$

    $\F{\G \v M : A_1 \ou A_2 \quad \G , x_1 : A_1 \v N_1 : C \quad
    \G , x_2 : A_2 \v N_2 : C} {\G \v (M\;[x_1.N_1,
    x_2.N_2]) : C} \, \ou_e$

4.  If $\approx$ is a congruence on ${\cal T}$ (resp. ${\cal T}'$), we define the systems ${\cal S}_{\approx}$, (resp. ${\cal
    S}^{\m}_{\approx}$, ${\cal S}^{\f\et\ou}_{\approx}$) as the system ${\cal S}$ (resp. ${\cal S}^{\m}$, ${\cal
    S}^{\f\et\ou}$) where we have added the 