diff --git a/RapportStage.tex b/RapportStage.tex
index e640ce1..ffc82a1 100644
--- a/RapportStage.tex
+++ b/RapportStage.tex
@@ -483,8 +483,9 @@
 		
 			Grâce à ces méthodes, nous pouvons réutiliser les règles de typage de Featherweight Java presque à l'identique, qui sont rappelées \autoref{fig:typti}. Nous avons enlevé la règle de typage \textsc{T-SCast} qui autorisait les casts que les auteurs qualifiaient de \enquote{stupides}, entre deux types qui n'étaient pas parents l'un de l'autre.
 			
-			Nous vérifions aussi évidement la \eng{class table} $\mathcal{B}$, en vérifiant que le corps de chaque méthode est bien typé par le type attendu dans la méthode, que les champs de la \eng{class table} ne contredisent pas la \eng{test interface}. On note alors $\mathcal{B} \OKin \mathfrak{T}$. Les seules contradictions sont grammaticales si l'on a déjà vérifié que les applications $\operatorname{fields}$, $\operatorname{construct}$ et $\operatorname{mtype}$ n'étaient pas redéfinies ou mal définies.
-			%TODO prouver l'affirmation
+			Nous vérifions aussi évidement la \eng{class table} $\mathcal{B}$, en vérifiant que le corps de chaque méthode est bien typé par le type attendu dans la méthode, que les champs de la \eng{class table} ne contredisent pas la \eng{test interface}. On note alors $\mathcal{B} \OKin \mathfrak{T}$.
+			%XXX Si le temps, rajouter cette ligne et la prouver
+			%Les seules contradictions sont grammaticales si l'on a déjà vérifié que les applications $\operatorname{fields}$, $\operatorname{construct}$ et $\operatorname{mtype}$ n'étaient pas redéfinies ou mal définies.
 			
 			\begin{figure}
 				\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
@@ -617,11 +618,12 @@
 			Nous allons maintenant étudier les propriétés de cette nouvelle définition du préordre.
 			
 			\begin{property}
-				\[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\]
+				\label{thm:hnewnew}
+				\[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow^* e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\]
 			\end{property}
 			
 			On peut prouver cette propriété inductivement en montrant qu'une expression ayant un nœud \enquote{\fj{new}} en nœud racine se réduira forcément en une expression ayant un nœud racine du même type, en inversant la relation de réduction.
-			%TODO Preuve complète
+			La preuve complète est présentée \autoref{anx:proofPt1Val}.
 			
 			\begin{property}
 				\[\mathcal{A} \pprec \mathcal{B} \implies \mathcal{A} \prec \mathcal{B}\]
@@ -762,11 +764,11 @@
 		\begin{fjlisting}
 			\fjclass{Optional}{}{
 				\fjmethod{Object}{orElse}{Object e}{e}
-			}
+			}\\
 			\fjclass[Optional]{Some}{\fjattr{value}}{
 				\fjmethod{Object}{orElse}{Object e}{this.value}
 			}\\
-			\fjclass[Optional]{None}{}{}\\
+			\fjclass[Optional]{None}{}{}
 		\end{fjlisting}
 	
 		Ces trois classes définissent la notion d'\fj{Optional} qui fonctionne comme \lstinline[language=Caml]|a' option| en OCaml, et qui peut contenir une valeur ou non. La méthode \fj{orElse} permet de récupérer la valeur contenue si elle est présente, ou de renvoyer le paramètre dans le cas contraire.
@@ -793,7 +795,7 @@
 			
 			Notez que le problème est le même sans la présence de la méthode \fj{getList}, on n'aurait alors pas pû discriminer les deux méthodes \fj{contains} pour un même argument, puisqu'il n'aurait alors pas été possible d'instancier un argument.
 			
-			Bien sûr, avec une class table de tests, il est possible de créer des objets \fj{IList} de la forme que l'on souhaite, et donc de discriminer ces deux méthodes, par exemple avec une liste infinie de \fj{0}.
+			Bien sûr, avec une \eng{class table} de tests, il est possible de créer des objets \fj{IList} de la forme que l'on souhaite, et donc de discriminer ces deux méthodes, par exemple avec une liste infinie de \fj{0}.
 		
 	\section{Preuve du théorème de cohérence du typage des \eng{test interfaces}}
 	\label{anx:proofTyptyp}
@@ -960,7 +962,52 @@
 			
 			\subparagraph{\textnormal{\textsc{\ref{rule:ti:downCast}}}}
 				Exactement la même preuve que le point précédent en appliquant la règle \textsc{T-DCast}
+		
+		\section{Preuve de la \autoref{thm:hnewnew} sur les valeurs infinies}
+			\label{anx:proofPt1Val}
+			Nous allons d'abord montrer la propriété sur les expressions suivante:
+			\begin{property}
+				\label{thm:enewnew}
+				Soit $e$ et $f$ des expressions fermées, telles que $e \rightarrow^* f$,
 				
+				Alors, si $e = \fj{new C($\overline{e'}$)}$
+				
+				On a $f = \fj{new C($\overline{f'}$)}$ et $\overline{e'} \rightarrow^* \overline{f'}$.
+			\end{property}
+		
+			Montrons cette propriété par récurrence sur la taille de la relation $e \rightarrow^* f$.
+			\subparagraph{Initialisation}
+				Dans le cas $e = f$, on a simplement $f = \fj{new C($\overline{e'}$)}$ et $\overline{e'} \rightarrow^0 \overline{e'}$.
+			\subparagraph{Hérédité}
+				Nous sommes dans l'hypothèse que $e \rightarrow^n f$
+				Observons la première relation. Elle se fait nécessairement sur un nœud de type \ref{rule:expr:method}, \ref{rule:expr:field} ou \ref{rule:expr:cast}, qui est donc contenu dans l'un des $\overline{e'}$. Donc, on a $e'_i \rightarrow e''_i$. On note $e''_k = e'_k$ pour $k$ différent de $i$, et on obtient que
+				\[e = \fj{new C($\overline{e'}$)} \rightarrow \fj{new C($\overline{e''}$)} \rightarrow^{n-1} f\]
+				On peut donc appliquer l'hypothèse de récurrence à la dernière relation $\rightarrow^{n-1}$, et nous obtenons bien que 
+				\[f = \fj{new C($\overline{f'}$)} \quad\text{et}\quad \overline{e'} \rightarrow^* \overline{e''} \rightarrow^* \overline{f'}\]
+				
+				La récurrence est bouclée.
+				
+			Nous allons donc pouvoir facilement montrer la \autoref{thm:hnewnew} par induction sur le paramètre $\hbar$.
+			
+			\subparagraph{$\hbar = \fj{x}$}
+				
+				Alors, en notant $\beta$ tel que $\beta(\fj{x}) = e'$.
+				
+				Alors,
+				\[\hbar\bracket{\alpha} = \alpha(\fj{x}) \rightarrow e' = \hbar\bracket{\beta}\]
+				
+			\subparagraph{$\hbar = \fj{new C($\overline{\hbar'}$)}$}
+				
+				Alors, par application de la \autoref{thm:enewnew}, on obtient que
+				\[e' = \fj{new C($\overline{e}$)} \quad\text{et}\quad \overline{\hbar\bracket{\alpha}} \rightarrow^* \overline{e}\]
+					
+				On peut alors appliquer l'hypothèse d'induction, et obtenir que
+				\[\overline{e} = \overline{\hbar\bracket{\beta_x}}\]
+				
+				Donc, en notant $\beta$ la concaténation des $\beta_x$, qui est possible puisque les noms de variables utilisés dans $\hbar$ sont tous distincts, on obtient le résultat
+				\[e' = \hbar\bracket{\beta}\]
+				
+			
 		\section{Preuve du \eng{context lemma} avec valeurs infinies}
 			\label{anx:proofHValCL}
 			
diff --git a/header.tex b/header.tex
index a372dd4..0df5064 100644
--- a/header.tex
+++ b/header.tex
@@ -70,6 +70,7 @@
 	\renewcommand{\figureautorefname}{\textsc{Figure}}
 	\renewcommand{\appendixautorefname}{Annexe}
 	\renewcommand{\theoremautorefname}{Théorème}
+	\providecommand\propertyautorefname{Propriété}
 	\providecommand\ruleautorefname{règle}
 }