- $A \approx B$ if and only if $A=C[u/x]$, $B=C[v/x]$, and $u \approx v$.

Pure and typed $\l C$-calculus
==============================

The $C2$ type system
--------------------

We present in this section the J-L. Krivine’s classical type system.

-   We add a constant $C$ to the pure $\l$-calculus and we denote by $\L C$ the set of new terms also called $\l C$-terms. We consider the following rules of reduction, called rules of head $C$-reduction.

    -   1\) $(\l x u) t t_1 ... t_n \f (u[t / x]) t_1 ... t_n$ for every $u, t, t_1,...,t_n \in
        \L C$.

    -   2\) $(C) t t_1 ... t_n \f (t) \l x (x)t_1 ... t_n$ for every $ t, t_1,...,t_n
        \in \L C$, $x$ being a $\l$-variable not appearing in $t_1,...,t_n$.

<!-- -->

-   For any $\l C$-terms $t,t'$, we shall write $t \p_C t'$ if $t'$ is obtained from $t$ by applying these rules finitely many times. We say that $t'$ is obtained from $t$ by head $C$-reduction.

-   A $\l C$-term $t$ is said $\b$-normal if and only if $t$ does not contain a $\b$-redex.

-   A $\l C$-term $t$ is said $C$-solvable if and only if $t \p_C (f)t_1,...,t_n$ where $f$ 