diff --git a/RapportStage.tex b/RapportStage.tex
index b8024f7..4941417 100644
--- a/RapportStage.tex
+++ b/RapportStage.tex
@@ -866,110 +866,100 @@
 				Notre hypothèse de récurrence, notée \textsc{(HR)} est la suivante:
 				\[\forall h \quad \varepsilon \prec \gamma \implies h\bracket{\varepsilon} \prec^{<n} h\bracket{\gamma}\]
 				
-				Nous allons continuer en faisant une induction sur $h$.
+				Nous aurons ensuite trois cas, suivant l'endroit où s'effectue la première étape de la réduction.
 				
-				\subparagraph{Cas $h = \fj{$h_0$.meth($\overline{h_1}$)}$}
+				\underline{La réduction se fait uniquement avec des nœuds de $h_x$}
+					Alors, on a $h_x \rightarrow h_x'$, et donc $h \rightarrow h'$ indépendamment du \eng{mapping} considéré et on peut appliquer \textsc{(HR)} qui nous donne que, puisque $h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}$, alors, on a 
+					\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\]
+					
+				\underline{La réduction se fait sur un nœud à l'interieur d'une variable $\fj{x}$ de $h_x$}
+					Alors, dans cette occurrence de la variable $\fj{x}$ dans $h_x$, nous avons une réduction de la forme suivante.
+					\[\varepsilon(\fj{x}) \rightarrow e^{\fj{x}}\]
+					Choisissons alors un nom de variable non utilisé dans $\epsilon$ et $\gamma$, ici noté $\fj{y}$, et créons $\varepsilon'$ ainsi:
+					
+					\[\varepsilon' = \left[ \begin{array}{ccc}
+						\fj{x} &\mapsto& \varepsilon(\fj{x})\\
+						\fj{y} &\mapsto& e^{\fj{x}}\\
+						v &\mapsto& \varepsilon(v)
+					\end{array} \right]
+					\quad
+					\gamma' = \left[ \begin{array}{ccc}
+						\fj{x} &\mapsto& \gamma(\fj{x})\\
+						\fj{y} &\mapsto& \gamma(\fj{x})\\
+						v &\mapsto& \gamma(v)
+					\end{array} \right]\]
 				
-					\underline{Cas 1} si la première réduction ne se fait pas sur la racine de $h$.
+					Ainsi, la réduction considérée s'exprime comme
+					\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\]
 					
-					Alors, dans l'un des $h_x\bracket{\varepsilon}$ on a que 
-					\[h_x\bracket{\varepsilon} \rightarrow e^0\]
+					Or, nous avons aussi que $\varepsilon' \prec \gamma'$. Nous n'avons en effet que $\varepsilon(\fj{y})\prec\gamma(\fj{y})$ à vérifier, c'est à dire que $\varepsilon(\fj{x})\rightarrow e^{\fj{x}} \prec \gamma(\fj{x})$
 					
-					Il y a alors trois possibilités:
-					
-					\underline{La réduction se fait uniquement avec des nœuds de $h_x$}
-						Alors, on a $h_x \rightarrow h_x'$, et donc $h \rightarrow h'$ indépendamment du \eng{mapping} considéré et on peut appliquer \textsc{(HR)} qui nous donne que, puisque $h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}$, alors, on a 
-						\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\]
+					Cela est vrai par propriété de confluence sur l'opération de réduction. 
+					\begin{center}
+					\begin{tikzpicture}
+						\node (e1) at (1,1) {$\varepsilon(\fj{x})$};
 						
-					\underline{La réduction se fait sur un nœud à l'interieur d'une variable $\fj{x}$ de $h_x$}
-						Alors, dans cette occurrence de la variable $\fj{x}$ dans $h_x$, nous avons une réduction de la forme suivante.
-						\[\varepsilon(\fj{x}) \rightarrow e^{\fj{x}}\]
-						Choisissons alors un nom de variable non utilisé dans $\epsilon$ et $\gamma$, ici noté $\fj{y}$, et créons $\varepsilon'$ ainsi:
+						\node (e2) at (0,0) {$e^{\fj{x}}$};
 						
-						\[\varepsilon' = \left[ \begin{array}{ccc}
-							\fj{x} &\mapsto& \varepsilon(\fj{x})\\
-							\fj{y} &\mapsto& e^{\fj{x}}\\
-							v &\mapsto& \varepsilon(v)
-						\end{array} \right]
-						\quad
-						\gamma' = \left[ \begin{array}{ccc}
-							\fj{x} &\mapsto& \gamma(\fj{x})\\
-							\fj{y} &\mapsto& \gamma(\fj{x})\\
-							v &\mapsto& \gamma(v)
-						\end{array} \right]\]
-					
-						Ainsi, la réduction considérée s'exprime comme
-						\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\]
+						\node (e3) at (0,-1) {$\hbar\bracket{\overline{e'}}$};
 						
-						Or, nous avons aussi que $\varepsilon' \prec \gamma'$. Nous n'avons en effet que $\varepsilon(\fj{y})\prec\gamma(\fj{y})$ à vérifier, c'est à dire que $\varepsilon(\fj{x})\rightarrow e^{\fj{x}} \prec \gamma(\fj{x})$
+						\node (e4) at (1,-2) {$\hbar\bracket{\overline{e''}}$};
 						
-						Cela est vrai par propriété de confluence sur l'opération de réduction. 
+						\draw[->] (e1) -- (e2);
+						\draw[->] (e2) to node[very near end, above right] {$*$} (e3);
 						
-						\begin{tikzpicture}
-							\node (e1) at (1,1) {$\varepsilon(\fj{x})$};
-							
-							\node (e2) at (0,0) {$e^{\fj{x}}$};
-							
-							\node (e3) at (0,-1) {$\hbar\bracket{\overline{e'}}$};
-							
-							\node (e4) at (1,-2) {$\hbar\bracket{\overline{e''}}$};
-							
-							\draw[->] (e1) -- (e2);
-							\draw[->] (e2) to node[very near end, above right] {$*$} (e3);
-							
-							\draw[->,dashed] (e1) to node[very near end, above right] {$*$} (e4);
-							\draw[->,dashed] (e3) to node[very near end, above right] {$*$} (e4);
-						\end{tikzpicture}
-					
-						On peut alors appliquer que $\varepsilon \prec \gamma$.
-						
-						Nous avons toutes les conditions réunies qui nous permettent d'appliquer l'hypothèse de récurrence.
-						
-					\underline{La réduction s'est faîte entre un nœud de $h$ et un nœud de $\varepsilon$}
-						Il y a deux cas de figure pour lesquels les deux cas précédents ne sont pas adéquats. Le premier est un appel à \eng{field} de la forme $\fj{x.field}$ et le second est un appel à méthode de la forme $\fj{x.meth($\overline{h'}$)}$.
-						\marginpar{Faut-il ajouter le cas du Cast ?}
-						
-						Dans ces deux cas, nous avons nécessairement $\varepsilon(\fj{x}) = \fj{new C($\overline{e^\varepsilon}$)}$, et donc aussi $\gamma(\fj{x}) = \fj{new C($\overline{e^\gamma}$)}$ avec $\overline{e^\varepsilon} \prec \overline{e^\gamma}$, puisque $\varepsilon \prec \gamma$.
-						
-						Dans le cas de $\fj{x.field}$, on choisit un nouveau nom de variable inutilisé $\fj{y}$, et nous créons une nouvelle fois $\varepsilon'$ et $\gamma'$ ainsi.
-		
-						\[\varepsilon' = \left[ \begin{array}{ccc}
-							\fj{x} &\mapsto& \varepsilon(\fj{x})\\
-							\fj{y} &\mapsto& e^\varepsilon_k\\
-							v &\mapsto& \varepsilon(v)
-						\end{array} \right]
-						\quad
-						\gamma' = \left[ \begin{array}{ccc}
-							\fj{x} &\mapsto& \gamma(\fj{x})\\
-							\fj{y} &\mapsto& e^\gamma_k\\
-							v &\mapsto& \gamma(v)
-						\end{array} \right]\]
-					
-						Nous avons alors toujours $\varepsilon' \prec \gamma'$, mais aussi que la première réduction s'écrit 
-						\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\]
-						où $h'$ est obtenu en remplaçant l'occurrence de $\fj{x.field}$ susnommée par $\fj{y}$.
-						
-						
-						On peut donc appliquer l'hypothèse de récurrence. pour obtenir, puisque les \eng{class table} considérées sont les mêmes
-						\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma'} \rightarrow^* \hbar\bracket{\overline{f'}}\]
-						
-						Dans le cas de $\fj{x.meth($\overline{h'}$)}$, la procédure est presque la même.
-						
-						Nous allons noter $\overline{v}$ les noms des paramètres de $\fj{C.meth}$. Nous noterons aussi $h_m$ le corps de cette méthode.
-						
-						Nous allons enfin obtenir $h_m'$ en remplacant dans $h_m$ la variable $\fj{this}$ par la variable $\fj{x}$ et les appels à chaque variable $v_k$ par l'expression à variables $h'_k$.
-						
-						Nous pouvons garder $\varepsilon$ et $\gamma$ tels qu'ils sont.
-						
-						Alors, en remplacant l'appel $\fj{x.meth($\overline{h'}$)}$ susnommé par $h_m'$ dans $h$, on obtient une nouvelle expression $h'$ telle que la réduction soit
-						\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\]
-						
-						Mais en ayant aussi que 
-						\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma}\]
-						
-						On peut enfin appliquer l'hypothèse de récurrence de la même manière.
-						
-					\underline{Cas 2} où la première réduction se fait sur la racine de $h$.
+						\draw[->,dashed] (e1) to node[very near end, above right] {$*$} (e4);
+						\draw[->,dashed] (e3) to node[very near end, above right] {$*$} (e4);
+					\end{tikzpicture}
+					\end{center}
 				
+					On peut alors appliquer que $\varepsilon \prec \gamma$.
+					
+					Nous avons toutes les conditions réunies qui nous permettent d'appliquer l'hypothèse de récurrence.
+					
+				\underline{La réduction s'est faîte entre un nœud de $h$ et un nœud de $\varepsilon$}
+					Il y a trois cas de figure pour lesquels les deux cas précédents ne sont pas adéquats. Le premier est un appel à \eng{field} de la forme $\fj{x.field}$, le second est un appel à méthode de la forme $\fj{x.meth($\overline{h'}$)}$ et le troisième cas est le \eng{cast} de la forme $\fj{(D)x}$.
+					
+					Dans ces trois cas, nous avons nécessairement $\varepsilon(\fj{x}) = \fj{new C($\overline{e^\varepsilon}$)}$, et donc aussi $\gamma(\fj{x}) = \fj{new C($\overline{e^\gamma}$)}$ avec $\overline{e^\varepsilon} \prec \overline{e^\gamma}$, puisque $\varepsilon \prec \gamma$.
+					
+					Dans le cas de $\fj{x.field}$, on choisit un nouveau nom de variable inutilisé $\fj{y}$, et nous créons une nouvelle fois $\varepsilon'$ et $\gamma'$ ainsi.
+	
+					\[\varepsilon' = \left[ \begin{array}{ccc}
+						\fj{x} &\mapsto& \varepsilon(\fj{x})\\
+						\fj{y} &\mapsto& e^\varepsilon_k\\
+						v &\mapsto& \varepsilon(v)
+					\end{array} \right]
+					\quad
+					\gamma' = \left[ \begin{array}{ccc}
+						\fj{x} &\mapsto& \gamma(\fj{x})\\
+						\fj{y} &\mapsto& e^\gamma_k\\
+						v &\mapsto& \gamma(v)
+					\end{array} \right]\]
+				
+					Nous avons alors toujours $\varepsilon' \prec \gamma'$, mais aussi que la première réduction s'écrit 
+					\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\]
+					où $h'$ est obtenu en remplaçant l'occurrence de $\fj{x.field}$ susnommée par $\fj{y}$.
+					
+					
+					On peut donc appliquer l'hypothèse de récurrence. pour obtenir, puisque les \eng{class table} considérées sont les mêmes
+					\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma'} \rightarrow^* \hbar\bracket{\overline{f'}}\]
+					
+					Dans le cas de $\fj{x.meth($\overline{h'}$)}$, la procédure est presque la même.
+					
+					Nous allons noter $\overline{v}$ les noms des paramètres de $\fj{C.meth}$. Nous noterons aussi $h_m$ le corps de cette méthode.
+					
+					Nous allons enfin obtenir $h_m'$ en remplacant dans $h_m$ la variable $\fj{this}$ par la variable $\fj{x}$ et les appels à chaque variable $v_k$ par l'expression à variables $h'_k$.
+					
+					Nous pouvons garder $\varepsilon$ et $\gamma$ tels qu'ils sont.
+					
+					Alors, en remplacant l'appel $\fj{x.meth($\overline{h'}$)}$ susnommé par $h_m'$ dans $h$, on obtient une nouvelle expression $h'$ telle que la réduction soit
+					\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\]
+					
+					Mais en ayant aussi que 
+					\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma}\]
+					
+					On peut enfin appliquer l'hypothèse de récurrence de la même manière.
+					
+					Enfin, dans le dernier cas $\fj{(D)x}$, puisque la réduction s'est bien effectuée, c'est que $\fj{C} \subclass \fj{D}$. On peut donc simplement remplacer dans $h$ le cast par la variable $\fj{x}$ seule.
 				
 \end{document}
diff --git a/header.tex b/header.tex
index 48e27a8..b8ef22e 100644
--- a/header.tex
+++ b/header.tex
@@ -111,9 +111,8 @@
 %%% Subparaghaphs box
 \newtcbox{\subparaghaphbox}{nobeforeafter,tcbox raise base, arc=9pt, outer arc=9pt, boxsep=2pt,left=2pt,right=2pt,top=2pt,bottom=2pt,boxrule=1pt,colback=white!85!orange}
 \newcommand{\subparaghaphboxedcontent}[1]{\subparaghaphbox{#1}\newline}
-\titleformat{\subparagraph}[runin]
-{\normalfont\normalsize\bfseries}{}{0em}{\subparaghaphboxedcontent}
-
+%\titleclass{\mathcases}{straight}[\subparagraph]
+\titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0em}{\subparaghaphboxedcontent}
 \titlespacing*{\subparagraph}{0pt}{3.25ex plus 1ex minus .2ex}{0.5em}
 
 %%% Blocs colorés pour le code FeatherweightJava