semantically that $x$ is an integer if and only if $x$ belongs to each set $X$ containing $0$ and closed under the successor function $s$.\
    The $\l$-term $\so{0} = \l x \l fx$ is of type $N[0]$ and represents zero.\
    The $\l$-term $\so{s} = \l n\l x\l
    f(f)((n)x)f$ is of type $\q y(N[y] \f N[s(y)])$ and represents the successor function.

-   A set of equations $E$ is said to be adequate with the type of integers if and only if :

    -   - $s(a) \not \approx 0$ ;

    -   - If $s(a) \approx s(b)$ , then so is $a \approx b$.

    In the rest of the paper, we assume that all sets of equations are adequate with the type of integers.

-   For each integer $n$, we define the Church integer $\so{n}$ by $\so{n} = \l x\l f(f)^n x$.

The integers in $AF2$
---------------------

The system $AF2$ has the property of the unicity of integers representation.

(see \[2\]) Let $n$ be an integer. If $\v_{AF2} t :N[s^n (0)]$, then $t \simeq\sb{\b}
\so{n}$.

The propositional trace $N=\q X \{ X,(X \f X) \f X \}$ of $N[x]$ also defines the integers.

(see \[2\]) If $\v_{AF2} t :N$, then, for a certain 