G'$\*, we check easily that $\v_{LAF2} \neg
    \neg \q X^{\ast} G'$\* $\f \q X^{\ast} G'$\*. $\Box$

Let $A,G$ be formulas of $LM2$, $t$ a term, $x$ a first order variable, and $X$ a second order variable. We have :\
1) $(A[t/x])$\*$= A$\*$[t/x]$.\
2) $(A[G/X])$\*$=A$\*$[G$\*$/X]$.

**Proof By induction on $A$. $\Box$**

Let $A$ be a formula of $LM2$, $G$ a classical type, and $X_C$ a classical variable.\
$\v_{LAF2} (A[G/X_C])$\*$ \equi A$\*$[\neg G$\*$/X_C]$.

**Proof By induction on $A$.**

-   - If $A = D(t_1,...,t_n)$ where $D$ is a predicate variable or a predicate symbol, then $A$\*=$A$, and $\v_{LAF2} A \equi  A$.

-   - If $A = X_C (t_1,...,t_n)$, then $A$\*=$\neg X^{\ast}(t_1,...,t_n)$, and, by Lemma 3.2, $\v_{LAF2} \neg \neg G$\*$ \equi G$\*.

-   - If $A = B \f C$, then $A$\* = $B$\* $\f$ $C$\*. By the induction hypothesis, we have $\v_{LAF2} (B[G/X_C])$\*$ \equi B$\*$[\neg G$\*$/X_C]$ and $\v_{LAF2}
    (C[G/X_C])$\*$ \equi C$\*$[\neg G$\*$/X_C]$. Therefore $\v_{LAF2} \{ (B[G/X_C])$\*$
    \f (B[G/X_C])$\*$\} \equi \{ B$\*$[\neg G$\*$/X_C] \f C$\*$[\neg G$\*$/X_C] \}$.

-   - If $A = \q vA'$, where $v=x$ or $v=X$, then $A$\*=$\q vA'$\*. By the induction hypothesis, we have $\v_{LAF2} (A'[G/X_C])$\*$ \equi A'$\*$[\neg G$\*$/X_C]$. Therefore $\v_{LAF2}
    (\q vA'[G/X_C])$\*$ \equi \q vA'$\*$[\neg G$\*$/X_C]$.

-   - If 