diff --git a/soundness.tex b/soundness.tex
index 5e9b2c0..cfd1272 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -21,7 +21,7 @@ TODO:
     \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
     \begin{description}
     \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
-    and $(\Delta, \sigma) = \unify{\Delta', C}$
+    and $(\Delta, \sigma) = \unify{}(\Delta', C)$
 %    , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
 %    and $\vdash \ol{L} : \mtypeEnvironment{}$
 %    and $\Gamma \subseteq \mtypeEnvironment{}$
@@ -63,6 +63,12 @@ By structural induction over the expression $\texttt{e}$.
 
     $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
 
+    % X.List<X> <. List<a?>
+    % $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
+    % $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
+    % TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
+    % by proofing every substitution in Unify is ok aslong as every type in the inputs is ok
+
     $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
     %Easy, because unify only generates substitutions for normal type placeholders which are OK