On se donne un ensemble $\CTyp\subseteq\FTyp$ et deux pr\'e-ordre bien fond\'e $\preced$, $\sqsubseteq$ sur $\CTyp$ tels que $\sqsubseteq$ est plus fin que $\preceq$ (ie $\preceq\subseteq\sqsubseteq$).
On se donne un ensemble $\CTyp\subseteq\FTyp$ et un pr\'e-ordre bien fond\'e $\preced$ sur $\CTyp$.
\end{defi}
\begin{defi}[Statut]
...
...
@@ -380,15 +380,14 @@ then $\Gamma\vdash t':T$.
\begin{defi}[Ordre sur les constructeurs de type]
Soit $C$ de statut $(i_1,\dots,i_n)$ et $C'$ de statut $(j_1,\dots,j_{n'})$.
On a $C\,\bar l\>C'\,\bar u$ si l'une des 3 conditions suivantes est remplie :
On a $C\,\bar l\>C'\,\bar u$ si l'une des 2 conditions suivantes est remplie :
\begin{itemize}
\item$C\succ C'$,
\item$C\approx C'$ et $(l_{i_1},\dots,l_{i_{\min(n,n')}})\rhd_{lex}(u_{j_1},\dots,u_{j_{\min(n,n')}})$,
\item$C\sqsupseteq C'$ et $(l_{i_1},\dots,l_{i_{\min(n,n')}})\trianglerighteq_{lex}(u_{j_1},\dots,u_{j_{\min(n,n')}})$,
\item$C\approx C'$ et $(l_{i_1},\dots,l_{i_{\min(n,n')}})\trianglerighteq_{lex}(u_{j_1},\dots,u_{j_{\min(n,n')}})$,
\end{itemize}
\end{defi}
Remarquons que l'ordre strict est d\'efini comme l'ordre large, sauf que $\sqsupset$ remplace $\sqsupseteq$ dans la derni\`ere condition.
Remarquons que l'ordre strict est d\'efini comme l'ordre large, sauf que $\rhd$ remplace $\trianglerighteq$ dans la derni\`ere condition.
\todo{Si chaque classe d'\'equivalence pour $\approx$ il existe un entier $n$ tel que les $st(C)$ sont de taille inf\'erieure \`a $n$,
