proof for one step of reduction. We have two cases :**

-   - If $t=(\l xu)vv_1...v_m$, then $t'=(u[v/x])v_1...v_m$, $\G,x:F \v_{C2_O} u:G$, $F$ and $G$ are not ending with $O$, $G'\lhd_O F_1 \f G_1$, $G'_j \lhd_O F_{j+1} \f G_{j+1}$ $1 \leq j
    \leq m-1$, $G_m \approx \perp$, $G_j \approx G'_j$ $1 \leq j \leq m-1$, $\G \v_{C2_O} v:F$, and $\G \v_{C2_O} v_j:F_j$ $1 \leq j \leq m$. It is easy to check that $\G \v_{C2_O} u[v/x]:G$, then $\G \v_{C2_O} t':\perp$.

-   - If $t=(C)vv_1...v_m$, then $t'=(v)\l x(x)v_1...v_m$, and there is a type $A$ which is not ending with $O$ such that : $A'\lhd_O F_1 \f G_1$, $G'_j \lhd_O F_{j+1} \f G_{j+1}$ $1 \leq j
    \leq m-1$, $G_m \approx \perp$, $A \approx A'$, $G_j \approx G'_j$ $1 \leq j \leq m$, $\G \v_{C2_O}
    v:\neg \neg A$, and $\G \v_{C2_O} v_j:F_j$ $1 \leq j \leq m$. It is easy to check that $\G,x:A \v_{C2_O} (x)v_1...v_m:\perp$, but $A$ is not ending with $O$, then $\G \v_{C2_O}
    \l x(x)v_1...v_m:\neg A$, and $\G \v_{C2_O} t':\perp$.

b\) Indeed, a typing of $C2_O$ may be seen as a typing of $C2$. $\Box$

a\) If $\G \v_{C2_O} t:O(a)$, and $t \p_C t'$, then $t=t'$.\
b) If $\G=y_1:A_1,...,y_n:A_n,x_1:O(a_1),...,x_m:O(a_m) \v_{C2_O} t:O(a)$, 