\in \O^+$ (resp. $B \in \O^-$).\
2) If $A \in \O^-$ and $A \lhd B \f C$, then $B \in \O^+$ and $C \in \O^-$.

**Proof Easy. $\Box$**

Let $A_1,...,A_n$ be $\q$-negative types, $A$ a $\q$-positive type of $AF2$ which does not end with $\perp$, $B_1,...,B_m$ classical types, and $t$ a $\b$-normal $\l C$-term.\
If $\G = x_1:A_1,...,x_n:A_n,y_1:B_1,...,y_m:B_m \v_{M2} t:A$, then $t$ is a normal $\l$-term, and $x_1:A_1,...,x_n:A_n \v_{AF2} t:A$.

**Proof We argue by induction on $t$.**

-   - If $t$ is a variable, we have two cases :

    -   - If $t=x_i$ $1 \leq i \leq n$, this is clear.

    -   - If $t=y_j$ $1 \leq j \leq m$, then $A=\q \sou{v} B$ where $B_j \lhd B'_j$ and $B'_j
        \approx B$. Therefore, by Lemma 3.1, $A$ is a classical type. A contradiction.

-   - If $t=\l x u$, then $\G,x:E \v_{M2} u:F$, and $A=\q \sou{v}( E' \f F')$ where $E \approx
    E'$, $F \approx F'$ and $\sou{v}$ does not appear in $\G$. First, by Lemma 4.1, $E \in \O^-$ and $F \in \O^+$, and then, by the induction hypothesis, $u$ is a normal $\l$-term, and $x_1:A_1,...,x_n:A_n,x:E \v_{AF2} u:F$. Therefore $t$ is a normal $\l$-term, and $x_1:A_1,...,x_n:A_n \v_{AF2} t:A$.

-   