$A$. $\Box$**

Properties of $M2$ type system
==============================

By corollary 3.1, we have that a formula is provable in system $LAF2$ if and only if it is provable in system $LC2$. This resultat is not longer valid if we decorate the demonstrations by terms. We will give some conditions on the formulas in order to obtain such a result.\
We define two sets of types of $AF2$ type system : $\O^+$ (set of $\q$-positive types), and $\O^-$ (set of $\q$-negative types) in the following way :

-   - If $A$ is an atomic type, then $A \in \O^+$, and $A \in \O^-$ ;

-   - If $T \in \O^+$, and $T' \in \O^-$, then, $T' \f T \in \O^+$, and $T \f T' \in \O^-$ ;

-   - If $T \in \O^+$, then $\q x T \in \O^+$ ;

-   - If $T \in \O^-$, then $\q x T \in \O^-$ ;

-   - If $T \in \O^+$, then $\q X T \in \O^+$ ;

-   - If $T \in \O^-$, and $X$ has no free occurence in $T$, then $\q X T \in \O^-$.

1\) If $A \in \O^+$ (resp. $A \in \O^-$) and $A \approx B$, then $B 