following typing rule.

    $$\F{\G \v M : A \;\;\; A \approx B}{\G \v M : B} \, \approx$$

-   We will denote by $size(M)$ the complexity of the term $M$.

-   Let $\overrightarrow{P}$ be a finite (possibly empty) sequence of terms and $M$ be a term. We denote by $(M \ \overrightarrow{P})$ the term $(M \ P_1 \ ... \ P_n)$ where $\overrightarrow{P}= P_1, ...,
    P_n$.

-   In the rest of the paper $\tr$ will represent the reduction determined by all the rules of the corresponding calculus.

-   If we want to consider only some of the rules we will mention them as a subscript of $\tr$. For example, in the $\l\m^{\f\et\ou}$-calculus, $M \tr_{\b\m} N$ means that $M$ reduces to $N$ either by the $\b$-rule or by the $\m$-rule.

-   As usual, $\tr_r^*$ (resp. $\tr_r^+$) denotes the symmetric and transitive closure of $\tr_r$ (resp. the transitive closure of $\tr_r$). We denote $M \tr_{r}^1 N$ iff $M = N$ or $M \tr_r N$.

-   A term $M$ is strongly normalizable for a reduction $\tr_r$ (denoted as $M \in SN_r$) if there is no infinite sequence of reductions $\tr_r$ starting from $M$. For $M \in SN_r$, we denote by $\eta_r(M)$ the length 