G$\*$ \f G$\* by induction on $G$.**

-   - If $G = \perp$, then $G$\*=$\perp$, and $\v_{LAF2} ((\perp \f \perp) \f \perp) \f
    \perp$.

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

-   - If $G = A \f B$, then $B$ is a classical type and $G$\* = $A$\* $\f$ $B$\*. By the induction hypothesis, we have $\v_{LAF2} \neg \neg B$\*$ \f B$\*. Since $\v_{LAF2} \neg \neg
    (A$\*$\f B$\*) $\f$ $(\neg \neg A$\*$\f \neg \neg B$\*), we check easily that $\v_{LAF2}
    \neg \neg (A$\* $\f B$\*) $\f (A$\* $\f B$\*).

-   - If $G = \q vG'$ where $v=x$ or $v=X$, then $G'$ is a classical type and $G$\*=$\q vG'$\*. By the induction hypothesis, we have $\v_{LAF2}
    \neg \neg G'$\*$ \f G'$\*. Since $\v_{LAF2} \neg \neg \q vG'$\* $\f$ $\q v \neg \neg G'$\*, we check easily that $\v_{LAF2} \neg \neg \q vG'$\* $\f \q vG'$\*.

-   - If $G = \q X_C G'$, then $G'$ is a classical type and $G$\*=$\q X^{\ast} G'$\*. By the induction hypothesis, we have $\v_{LAF2} \neg \neg G'$\*$ \f G'$\*. Since $\v_{LAF2} \neg \neg \q
    X^{\ast} G'$\* $\f$ $\q X^{\ast} \neg \neg 