diff --git a/soundness.tex b/soundness.tex
index 4d1c5e8..c1608ee 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -106,6 +106,13 @@ $\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\
 
 %TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
 % and which is a supertype of T_r (so no free variables in T_r)
+
+We could use unify to generate S by
+$\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$
+%TODO: Proof that this always works.
+% Only the variables in \Delta' ol\Delta are used. Maybe change the lemma 10 to that.
+% That part of the unify algorithm is not influenced by other free variables
+
     This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
     $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
     $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,