diff --git a/soundness.tex b/soundness.tex
index 24b3581..d4577dc 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -1,5 +1,14 @@
 \section{Soundness}
 
+The differenciation of wildcard placeholders and normal type placeholders is vital for the soundness proof.
+During a let statement the environment $\Delta$ is extended by capture converted wildcards,
+but only for the scope of the body of the let statement.
+The capture converted wildcards must not be used outside of the let statement.
+This is ensured by two things:
+The first is lemma \ref{lemma:freeVariablesOnlyTravelOneHop} which ensures that free variables only
+travel one hop at the time through a constraint set.
+And the second one is the fact that normal type placeholders never contain free variables.
+
 % \begin{lemma}
 % A sound TypelessFJ program is also sound under LetFJ type rules.
 % \begin{description}
@@ -150,14 +159,14 @@ $\sigma(\tv{a}) = \type{T}_2$ then
 First we can say $\Delta | \Gamma \vdash \expr{x} : \type{N}$ by T-Var.
 %$\Delta, \Delta', \overline{\Delta} \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
 %and lemma \ref{lemma:unifySoundness}.
-%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:unifyNoFreeVariablesInSupertype}:
+%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:freeVariablesOnlyTravelOneHop}:
 %$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$
 %by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
-%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:unifyNoFreeVariablesInSupertype}.
+%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}.
 By lemma \ref{lemma:unifyWellFormedness} and WF-Var we can deduct
 $\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \Delta$ 
 and by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
-and lemmas \ref{lemma:unifySoundness} and \ref{lemma:unifyNoFreeVariablesInSupertype}
+and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}
 we can finally say 
 $\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$.
 With the constraint $\tv{a} \doteq [\ol{\wtv{a}}/\ol{X}]\type{T}$
@@ -167,7 +176,7 @@ we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_
 \end{itemize}
 
 % method call: a1 <c C<a>, a2 <c C<b>, a3 <c b?
-% here lemma:unifyNoFreeVariablesInSupertype can be used too
+% here lemma:freeVariablesOnlyTravelOneHop can be used too
 
     %TODO: use a lemma that says if Unify succeeds, then it also succeeds if the capture converted types are used.
     % but it also works with a subset of the initial constraints.
@@ -237,6 +246,14 @@ we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_
     % $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
     % %Easy, because unify only generates substitutions for normal type placeholders which are OK
 
+\item[$\text{let}\ \expr{x} = \expr{e} \ \text{in}\ 
+\text{let}\ \overline{\expr{x} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x})$]
+generates constraints $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
+\tv{r} \lessdot \tv{a}, \ol{\tv{x}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{r}, \ol{\wtv{b}} \lessdot \ol{N}$.
+We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \,
+\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$
+where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$,  $\sigma(\tv{a}) = \type{T}_2$.
+
     \item[$\texttt{v}.\texttt{m}(\ol{v})$]
     Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise.
     We know that $\unify{}(\Delta, [\overline{\wtv{b}}/\ol{Y}]\set{
@@ -621,7 +638,7 @@ Same as Subst
 \end{description}
 
 \begin{lemma}
-\label{lemma:unifyNoFreeVariablesInSupertype}
+\label{lemma:freeVariablesOnlyTravelOneHop}
 A constraint $\tv{a} \lessdotCC \type{T}$ or $\tv{a} \lessdot \type{T}$ implies that
 $\text{fv}(\sigma(\type{T})) \subseteq \text{fv}(\sigma(\tv{a}))$.
 Only free variables, which are part of the left side are used on the right side.