diff --git a/soundness.tex b/soundness.tex
index 9f4b849..c076b44 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -107,7 +107,7 @@ A correct typing for method calls can be deducted from those type informations.
 %    \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
 %    and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
     %\item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma  \vdash |\texttt{e}| : \sigma(\tv{a})$
-    \item[then] $\Delta,\Delta'|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$
+    \item[then] $\Delta|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$ where $\Delta = \Delta_u \cup \Delta'$
     \end{description}
 \end{lemma}
 % Regular type placeholders represent type annotations.
@@ -135,6 +135,33 @@ By structural induction over the expression $\texttt{e}$.
         and $\Delta, \Delta' \vdash  \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness}
         given the constraint $\tv{e}_2 \lessdot \tv{a}$.
     \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$]
+The let statement in the input is untyped and we have to create a let statement
+$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$
+that suffices the T-Let and T-Field type rules.
+The case where no capture conversion is needed, because $\Delta' = \emptyset$, is trivial. Here the Let statement can be skipped entirely.
+We investigate the case $\sigma(\tv{x}) = \wcNtype{\Delta}{N}$.
+%Constraints t1 <. x, x <. C<a>, T <. t2
+Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$ then
+\begin{itemize}
+\item $\Delta | \Gamma \vdash t_1 : \type{T}_1$ by assumption
+\item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ by constraint $\tv{t_1} \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}
+\item $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$
+$\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}:
+$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$
+
+% The constraint a =. [a?/X]T finishes this case
+
+%TODO: WIP
+
+We know $\type{T}_2 f \in \text{fields}(\type{N})$ because 
+
+
+\item $\Delta, \Delta' | \Gamma \vdash t_1 : \type{T}_1$ by lemma \ref{lemma:unifySoundness} and the constraint $\tv{t_1} \lessdot \tv{x}$
+\end{itemize}
+
     %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.
     % the generated constraints do not share wildcard placehodlers with other constraints.
@@ -586,6 +613,12 @@ $\sigma(\wildcardEnv) = \sigma([\type{T}/\tv{a}]\wildcardEnv)$
 Same as Subst
 \end{description}
 
+\begin{lemma}
+\label{lemma:unifyNoFreeVariablesInSupertype}
+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.
+\end{lemma}
 
 % \subsection{Converting to Wild FJ}
 % Wildcards are existential types which have to be \textit{unpacked} before they can be used.