- If $t=(x)u_1 ... u_r$ $r \geq 1$, we have two cases :

    -   - If $t=x_i$ $1 \leq i \leq n$, then $A_i \lhd B_1 \f C_1$, $C'_i \lhd B_{i+1} \f
        C_{i+1}$ $1 \leq i \leq r-1$, $C'_r \lhd D$, $A = \q vD'$, where $C'_i \approx C_i$ $1
        \leq i \leq r$, $D' \approx D$, and $\G \v_{M2} u_i:B_i$ $1 \leq i \leq r$. Since $A_i$ is a $\q$-negative types, we prove (by induction and using Lemma 4.1) that for all $1 \leq i \leq r$ $B_i$ is a $\q$-positive types. By the induction hypothesis we have $u_i$ is a normal $\l$-term, and $x_1:A_1,...,x_n:A_n \v_{AF2} u_i:B_i$. Therefore $t$ is a normal $\l$-term, and $x_1:A_1,...,x_n:A_n \v_{AF2} t:A$.

    -   - If $t=y_j$ $1 \leq j \leq m$, then $B_j \lhd B_1 \f
        C_1$, $C'_i \lhd B_{i+1} \f C_{i+1}$ $1 \leq i \leq r-1$, $C'_r \lhd D$, $A = \q vD'$, where $C'_i \approx C_i$ $1 \leq i \leq r$, $D' \approx D$, and $\G \v_{M2} u_i:B_i$ $1 \leq i
        \leq r$. Therefore, by Lemma 3.1, $A$ is a classical type. A contradiction.

-   - If $t=(C)uu_1 ... u_r$ $r \geq 0$, then there is a classical type $E$ such that 