and all $A_i$ $1 \leq i\leq
n$ are not ending with $O$, then $t$ is one of $x_i$, and $a_i \approx a$ $1 \leq i \leq n$.

**Proof a) It is enough to do the 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 O(a)$, $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$. Therefore $G_j$ $1 \leq j \leq m$ is not ending with $O$, which is impossible since $G_m \approx O(a)$.

-   - 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 O(a)$, $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$. $A$ is not ending with $O$, therefore $G_j$ $1 \leq j \leq m$ is not ending 