for every distinct variables $x,g,x_0,x_1,...,x_m$ :

    -   $(\th_n) x g x_0 \p_C (g) t_1 x_{r_0}$ ;

    -   $(t_i) x_i \p_C (g) t_{i+1} x_{r_i}$ $1\leq i\leq m$ ;

    -   $(t_m) x_m \p_C (x) x_{r_m}$ ;

    where $I(0)=n$, $I(r_m)=0$, and $I(i+1)=I(r_i)-1$ $0\leq i\leq m-1$.

We will generalize this result.\
Let $O$ be a particular unary predicate symbol. The typed system $C2_O$ is the typed system $C2$ where we replace the rules (2) and (7) by :

-   $(2_O)$ If $\G,x:A \v_{C2_O} t:B$, $A$ and $B$ are not ending with $O$, then $\G
    \v_{C2_O} \l xt:A \f B$.

-   $(7_O)$ If $\G\v_{C2_O} t:\q X A$, and $G$ is not ending with $O$, then $\G \v_{C2_O}
    t:A[G/X]$.

We define on the types of $C2_O$ a binary relation $\lhd_O$ as the least reflexive and transitive binary relation such that :

-   $\q xA \lhd_O A[u/x]$ if $u$ is a term of language ;

-   $\q XA \lhd_O A[G/X]$ if $G$ is a type which is not ending with $O$.

a\) If $\G \v_{C2_O} t:\perp$, and $t \p_C t'$, then $\G \v_{C2_O} t':\perp$.\
b) If $\G \v_{C2_O} t:A$, and $A$ is an atomic type, then $t$ is $C$-solvable.

**Proof a) It is enough to do the 