$n$, $t \simeq\sb{\b} \so{n}$.

**Remark A very important property of data type is the following (we express it for the type of integers) : in order to get a program for a function $f : N \f N$ it is sufficient to prove $\v
\q x ( N[x] \f N[f(x)] )$. For example a proof of $\v \q x ( N[x] \f N[p(x)] )$ from the equations $p(0)=0$, $p(s(x))=x$ gives a $\l$-term for the predecessor in Church intergers (see \[2\]). $\Box$**

The integers in $C2$
--------------------

The situation in system $C2$ is more complex. In fact, in this system the property of unicity of integers representation is lost and we have only one operational characterization of these integers.\
Let $n$ be an integer. A classical integer of value $n$ is a closed $\l C$-term $\th_n$ such that $\v_{C2} \th_n :N[s^n(0)]$.

(see \[6\] and \[12\]) Let $n$ be an integer, and $\th_n$ a classical integer of value $n$.

-   - if $n=0$, then, for every distinct variables $x,g,y$ : $(\th_n) x g y \p_C (x) y$ ;

-   - if $n \not = 0$, then there is $m \geq 1$ and a mapping $I
    : \{0,...,m \} \f N$, such that 