u) v$\], or is in head normal form \[i.e. $t=\l x_1 ...\l x_n (x) v_1 ... v_m$\]. The notation $u \p v$ means that $v$ is obtained from $u$ by some head reductions. If $u \p v$, we denote by $h(u,v)$ the length of the head reduction between $u$ and $v$.

(see\[3\])\
1) If $u \p v$, then, for any substitution $\s$, $\s(u) \p \s(v)$, and $h(\s(u),\s(v))$=h(u,v).\
2) If $u \p v$, then, for every sequence of $\l$-terms $\sou{w}$, there is a $w$, such that $(u)\sou{w} \p w$, $(v)\sou{w} \p w$, and $h((u)\sou{w},w)=h((v)\sou{w},w)+h(u,v)$.

**Remark. Lemma 2.1 shows that to make the head reduction of $\s(u)$ (resp. of $(u)\sou{w}$) it is equivalent - same result, and same number of steps - to make some steps in the head reduction of $u$, and after make the head reduction of $\s(v)$ (resp. of $(v)\sou{w}$). $\Box$**

-   The types will be formulas of second order predicate logic over a given language. The logical connectives are $\perp$ (for absurd), $\f$, and $\q$. There are individual (or first order) variables denoted by $x,y,z,...,$ and predicate (or second order) variables denoted by $X,Y,Z,....$

-   We do not suppose that the language has a special constant for equality. 