$\G \v_{M2}
    u:\neg \neg E$, $E \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. $\Box$

Let $A$ be a $\q$-positive type of $AF2$ and $t$ a $\b$-normal $\l C$-term.\
If $\v_{M2} t:A$, then $t$ is a normal $\l$-term, and $\v_{AF2} t:A$.

**Proof We use Theorem 4.1. $\Box$\
As for relation betwen the systems $C2$ and $M2$, we have the following result.**

Let $A_1,...,A_n,A$ be types of $C2$, and $t$ a $\l C$-term.\
$A_1,...,A_n \v_{C2} t:A$ if and only if $A_1^C,...,A_n^C \v_{M2} t:A^C$.

**Proof By induction on the typing of $t$. $\Box$**

The integers
============

-   Each data type can be defined by a second order formula. For example, the type of integers is the formula : $N[x]= \q X \{ X(0), \q y(X(y) \f X(sy)) \f X(x) \}$ where $X$ is a unary predicate variable, $0$ is a constant symbol for zero, and $s$ is a unary function symbol for successor. The formula $N[x]$ means 