diff --git a/soundness.tex b/soundness.tex
index 9c4eeee..398fe56 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -235,15 +235,10 @@ If there is a solution for a constraint set $C$, then there is also a solution f
     \item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$
     \item[then] $ (\sigma', \Delta') = \unify{}( C')$
 \end{description}
-\textit{Proof:}
-%TODO
 
 \end{lemma}
 \textit{Proof:}
-%TODO: is it true even?
-The input set does not contain free variables, only free variable placeholders.
-The only time \unify{} add a wildcard to the $\wildcardEnv$ is the \rulename{Capture} rule.
-This rule is only applied for the outer wildcard environments for each type.
+%TODO
 
 \begin{lemma}\label{lemma:unifySoundness}
 The \unify{} algorithm only produces correct output.