diff --git a/constraints.tex b/constraints.tex
index edee927..75a7e43 100644
--- a/constraints.tex
+++ b/constraints.tex
@@ -175,7 +175,7 @@ Those type variables count as regular types and can be held by normal type place
                       \orCons\set{
                       \set{ &
                       \tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
-                      [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
+                      \tv{a} \doteq [\overline{\wtv{a}}/\ol{X}]\type{T},
                       \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
                       } \\
                       & \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}
diff --git a/soundness.tex b/soundness.tex
index c076b44..24b3581 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -141,27 +141,34 @@ 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
+Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$,
+$\sigma(\tv{a}) = \type{T}_2$ 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}$
+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}:
+%$\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}.
+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}
+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}$
+and $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) \in \text{fields}(\sigma(\exptype{C}{\ol{\wtv{a}}}))$ by F-Class
+we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$.
+\item $\Delta, \Delta' \vdash \type{T}_2 <: \type{T}$ by constraint %TODO: Rename constraints
 \end{itemize}
 
+% method call: a1 <c C<a>, a2 <c C<b>, a3 <c b?
+% here lemma:unifyNoFreeVariablesInSupertype 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.
     % the generated constraints do not share wildcard placehodlers with other constraints.