diff --git a/soundness.tex b/soundness.tex
index 23160c5..3192f93 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -156,6 +156,12 @@ We have to show T-Let and T-Call which leaves us with:
 
 \end{description}
 
+\begin{lemma}
+    Free variables never leave their scope.
+    If $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
+    \tv{r} \lessdot \tv{a}$ % TODO
+\end{lemma}
+
 % \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
 % \begin{description}
 %     \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$