diff --git a/Richer.tex b/Richer.tex
index fba97437174691111cb071a5ff637cb9fa173676..c6832734771b37722013f64f65eb3f06e946fd08 100644
--- a/Richer.tex
+++ b/Richer.tex
@@ -133,7 +133,8 @@ Remarquons que l'ordre strict est d\'efini comme l'ordre large, sauf que ``$F\in
 il existe un entier $n$ tel que les $st(C)$ sont de taille inférieure à $n$,
 alors $>$ est bien fondé.}
 
-\todo{On aimerait utiliser ce que l'on d\'efinit un peu plus tard dans cette d\'efinition, que ce soit $\rhd_{acc}$ pour pouvoir g\'erer un constructeur de type $(f:Nat\impli Ord)\impli((n:Nat)\impli T\,(f\,n))\impli T\,(lim\,n)$, ou SCT pour ne pas se restreindre \`a un ordre lexicographique. (Attention ici, la pr\'esence de = sur la diagonale des boucles idempotentes ne suffit pas dans le cas o\`u l'on d\'esire un inf\'erieur large).}
+\todo{On aimerait utiliser ce que l'on d\'efinit un peu plus tard dans cette d\'efinition, que ce soit $\rhd_{acc}$ pour pouvoir g\'erer un constructeur de type $(f:Nat\impli Ord)\impli((n:Nat)\impli T\,(f\,n))\impli T\,(lim\,n)$, ou SCT pour ne pas se restreindre \`a un ordre lexicographique. (Attention ici, la pr\'esence de = sur la diagonale des boucles idempotentes ne suffit pas dans le cas o\`u l'on d\'esire un inf\'erieur large).
+On doit pouvaoir en revanche envisager le plus grand ordre large compatible avec l'ordre strict induit par SCT.}
 
 \begin{defi}[Types gel\'es]
   Pour $F\in\FTyp'$, $\bar t$ des termes tels que $\valabs{\bar t}=\arity(F)$, on d\'efinit les deux grammaires :
@@ -188,6 +189,12 @@ Dans cette d\'efinition, $\alpha$ est un ordinal, $\mu$ est un ordinal limite, $
     \bigcup_{X<Y}\overline{\interp{\Type}_X}\cup\enscond{C\,\bar t\in\VTyp}{C\,\bar t\approx Y}\\
   \omit\rlap{$\overline{\interp{\Type}_X}$ est le point fixe de la suite  croissante $\paren{\interp{\Type}^\alpha_X}_\alpha$}
 \end{align*}
+
+\end{defi}
+
+\remark{Pour que cette définition soit une ``bonne définition'', il faut que pour tout $A\in\interp{\Type}^\alpha_X$, l'on puisse définir $\interp{A}$.}
+
+\begin{defi}
 Soit $C\,\bar t\in\VTyp$ avec $C\in\CTyp$.
 On d\'efinit alors $\bar C=\enscond{C'\in\CTyp}{C'\approx C}=(C_1,\dots,C_n)$, o\`u l'on omet la conversion entre ensemble et tuple pour des questions de lisibilit\'e.
 On d\'efinit alors :
@@ -213,10 +220,14 @@ On d\'efinit alors :
 avec $R_{C\bar t}(T,(X_k))=
         \left\{
           \begin{array}{ll}
-            X_i& \text{s'il y a des }\bar l\text{ tels que }T=C_i\,\bar l\\
-
+            X_i& \text{s'il y a des }\bar l\text{ tels que }T=C_i\,\bar l\text{ et }C\,\bar t\approx C_i\,\bar l\\
+            \multicolumn{2}{l}{\enscond{t\in\Lm}{\text{pour tout }u\in R_{C\bar t}(T_1,\bar X),t\,u\in R_{C\bar t}(\subst{T_2}{x}{u},\bar X)}\text{ si }T=(x:T_1)\impli T_2}\\
+            \interp{C'\bar u}&\text{si }T=C'\,\bar u\text{ et }C'\,\bar u<C\,\bar t\\
           \end{array}
-        \right.
+        \right.$
 \end{defi}
 
+\remark{Pour que cette définition soit une ``bonne définition'',
+il faut que pour tout $C'\,\bar u<C\,\bar t$, $\interp{C'\,\bar u}$ soit défini.}
+
 \end{document}