answers to the previous questions.\
We present at the end (without proof) a similar result in the M. Parigot’s $\l
\m$-calculus.\
**Acknowledgement. We wish to thank J.L. Krivine, and C. Paulin for helpful discussions. We don’t forget the numerous corrections and suggestions from R. David and N. Bernard.**

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

-   Let $t,u,u_1,...,u_n$ be $\l$-terms, the application of $t$ to $u$ is denoted by $(t)u$. In the same way we write $(t)u_1...u_n$ instead of $(...((t)u_1)...)u_n$.

-   $Fv(t)$ is the set of free variables of a $\l$-term $t$.

-   The $\b$-reduction (resp. $\b$-equivalence) relation is denoted by $u \f\sb{\b} v$ (resp. $u
    \simeq\sb{\b} v$).

-   The notation $\s(t)$ represents the result of the simultaneous substitution $\s$ to the free variables of $t$ after a suitable renaming of the bounded variables of $t$.

-   We denote by $(u)^n v$ the $\l$-term $(u)...(u)v$ where $u$ occurs $n$ times, and $\sou{u}$ the sequence of $\l$-terms $u_1,...,u_n$. If $\sou{u} = u_1,...,u_n$ $n \geq 0$, we denote by $(t)\sou{u}$ the $\l$-term $(t)u_1...u_n$.

-   Let us recall that a $\l$-term $t$ either has a head redex \[i.e. $t=\l x_1 ...\l
    x_n (\l x u) v v_1 ... v_m$, the head redex being $(\l x 