system ${\cal S}^{\m}_{\approx}$ is strongly normalizing.

Let $M \in {\cal M}'$ be a term typable in ${\cal
S}^{\m}_{\approx}$. By lemma \[sn1-&gt;sn2\], it is enough to show that $M^{\diamond} \in SN_{\b}$. This follows immediately from theorem \[mendler\] and lemma \[coding3\]. Note that, in [@DaNo3], we also had given a direct proof of this result.

Strong normalization of ${\cal
    S}^{\f\et\ou}_{\approx}$
------------------------------

Let ${\cal F}=\{F_i \; / \; i \in I \}$ be a set of types in ${\cal T}'$ and let ${\cal F}^{\circ}=\{F_i^{\circ} \; / \; i \in I \}$ be its translation in ${\cal T}$. Let $\approx$ be the congruence generated by ${\cal F}$ in ${\cal T}'$ and let $\approx^{\circ}$ be the congruence generated by ${\cal F}^{\circ}$ in ${\cal T}$.

\[good\]

1.  If $\approx$ is good, then so is $\approx^{\circ}$.

2.  If $A \approx B$, then $A^{\circ} \approx^{\circ} B^{\circ}$.

<!-- -->

1.  Just note that $A_1^{\circ}$ and $A_2^{\circ}$ are in positive position in $\{A_1 \et A_2\}^{\circ}$ and $\{A_1 \ou A_2\}^{\circ}$.

2.  By induction on the proof of $A \approx B$.

\[coding4\] If $\G \v_{{\cal S}^{\f\et\ou}_{\approx}} M : A$, then $\G^{\circ}
\v_{{\cal S}^{\m}_{{\approx}^{\circ}}} M^{\circ} : A^{\circ}$.

By induction on a derivation of $\G \v_{{\cal S}^{\f\et\ou}_{\approx}}
M : A$.

\[mend\_3\] If $\approx$ is 