diff --git a/soundness.tex b/soundness.tex
index c0cd632..0c6bf63 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -89,7 +89,6 @@ By structural induction over the expression $\texttt{e}$.
 
     % T_r <: C<T> (S is in T)
     % Is C<T> ok?
-    % we could proof: \Delta' |- C<T> ok (\Delta' are all Wildcards used in Unify)
     % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
     % this together with the X <. N constraints proofs T_r ok
 
@@ -155,6 +154,15 @@ Method calls generate multiple constraints that share the same wildcard placehol
 % $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
 % %UNIFY fails when there are free variables on the right side of a a =. T constraint
 
+\begin{lemma}
+\unify{} generates well-formed type environments
+\begin{description}
+\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$
+\item[and] $\forall \Delta_w \in C: \vdash \type{L} <: \type{U}$ 
+\item[then] TODO
+\end{description}
+\end{lemma}
+
 \begin{lemma}
     Well-formedness is hereditary
     \begin{description}