is a variable.

It is easy to prove that : if $t \p_C t'$, then, for any substitution $\s$, $\s (t) \p_C \s
(t')$.

-   We add to the $AF2$ type system the new following rule :

    \(0) $\G \v C : \q X \{ \neg \neg X \f X \}$

    This rule axiomatizes the classical logic over the intuitionistic logic. We call $C2$ the new type system, and we write $\G \v_{C2} t : A$ if $t$ is of type $A$ in the context $\G$.

It is clear that $\G \v_{C2} t : A$ if and only if $\G , C : \q X \{ \neg \neg X \f X \} \v_{AF2} t :
A$.

(see \[6\])\
1) If $\G \v_{C2} t:A$, and $t \f_{\b} t'$, then $\G \v_{C2} t':A$.\
2) If $\G \v_{C2} t:\perp$, and $t \p_C t'$, then $\G \v_{C2} t':\perp$.\
3) If $A$ is an atomic type, and $\G \v_{C2} t:A$, then $t$ is $C$-solvable.

The $M2$ type system
--------------------

In this section, we present the system $M2$. This system allows essentialy to distinguish between classical proofs and intuitionistic proofs\
We assume that for every integer $n$, there is a countable set of special $n$-ary second 