$lg_{\b\m}(L^{\circ} \tr_{\b\m\r\th}^* R) \geq 1$. Then, by lemma \[diag\*\], there is a $P \in {\cal M}'$ such that $Q
\tr_{\b\m\r\th}^* P$, $R \tr_{\r}^* P$ and $lg_{\b\m}(Q
\tr_{\b\m\r\th}^* P) \geq lg_{\b\m}(L^{\circ} \tr_{\b\m\r\th}^* R)
\geq 1$. Thus $M^{\circ} \tr_{\b\m\r\th}^* P$, $N^{\circ} \tr_{\r}^*
P$ and $lg_{\b\m}(M^{\circ} \tr_{\b\m\r\th}^* P) \geq lg(M \tr^* N)$.

\[fin\] Let $M \in {\cal M}''$ be such that $M^{\circ} \in
SN_{\b\m\r\th}$. Then $M \in SN$.

Since $M^{\circ} \in SN_{\b\m\r\th}$, let $n$ be the maximum of $\tr_{\b\m}$ steps in the reductions of $M^{\circ}$. If $M \not
\in SN$, by lemma \[SNrth\], let $N$ be such that $M \tr^* N$ and $lg_{\b\m}(M \tr^* N) \geq n+1$. By lemma \[simulation3\], there is $P$ such that $M^{\circ} \tr_{\b\m\r\th}^* P$ and $lg_{\b\m}(M^{\circ} \tr_{\b\m\r\th}^* P) \geq lg_{\b\m}(M \tr^*
N)\geq n+1$. Contradiction.

\[SN2\] Every typed $\l\m^{\f\et\ou}$-term is strongly normalizable.

A consequence of theorems \[SN\_M\], \[retardemant\] and lemmas \[fin\], \[coding2\].

Recursive equations on types {#7}
============================

We study here systems where equations on types are allowed. These types are usually called recursive types. The subject reduction and the decidability of type assignment are preserved but the strong normalization may be lost. For example, with the equation $X = X \f
T$, the term $(\D \; \D)$ where $\D=\l 