diff --git a/constraints.tex b/constraints.tex
index c1dccd3..7a7b719 100644
--- a/constraints.tex
+++ b/constraints.tex
@@ -112,7 +112,7 @@ Wildcard types are not used during the constraint generation step and have no in
                     & \constraint = \begin{array}[t]{@{}l@{}l}
                       \orCons\set{
                       \set{ &
-                      \tv{r} \lessdot \exptype{C}{\ol{\wtv{a}}} ,
+                      \tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
                       [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} , \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 97796af..c820760 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -17,14 +17,13 @@ Type inference produces a correctly typed program.
     \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
     \begin{description}
     \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
-    , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdot \type{T'} } }$
-    and $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
-    and $\vdash \ol{L} : \mtypeEnvironment{}$
-    and $\Gamma \subseteq \mtypeEnvironment{}$
-    \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'})}$
-    %and $\Delta \vdash \sigma(\type{S}), \sigma(\type{T})\ \ok$
-    \item[then] $\Delta|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$
+    and $(\Delta, \sigma) = \unify{\Delta', C}$
+%    , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
+%    and $\vdash \ol{L} : \mtypeEnvironment{}$
+%    and $\Gamma \subseteq \mtypeEnvironment{}$
+%    \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] $\Delta|\Gamma  \vdash |\texttt{e}| : \sigma(\tv{a})$
     \end{description}
 \end{lemma}
 Regular type placeholders represent type annotations.
@@ -41,23 +40,26 @@ used in let statements and as type parameters for generic method calls.
 \textit{Proof:}
 By structural induction over the expression $\texttt{e}$.
 \begin{description}
-    \item[$\texttt{e}.\texttt{f}$] $\Delta|\Gamma  \vdash \texttt{e} : \sigma(\tv{r})$ by assumption.
-    $\Delta', \Delta\vdash \CC{}(\sigma(\tv{r})) <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
-    Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
-    %TODO: Proof this: The reason is that r is not flagged with a ? and we only add free variables here, that are in \Delta
-    Then $\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \text{dom}(\Delta)$
-    and therefore $\text{fv}(\type{N}) \subseteq \text{dom}(\Delta, \Delta')$.
-    This implies $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$,
-    because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$
-    and $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
+    \item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
+    then $\Delta|\Gamma  \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
+    $\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
+    %Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
+    Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
+    
+    The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
+    
+    We now show
+    $\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
+    by the T-Field rule.
+    $\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
+    $\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
+    because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
+    $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
     and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.
 
-%    Set $\sigma(\tv{r}) = \type{T} = \wcNtype{\Delta'}{N}$.
-%    Then $\Delta | \Gamma \vdash e : \type{T}$ by assumption. $\Delta \vdash \type{T} <: \wcNtype{\Delta'}{N}$ by S-Refl.
-%    $\textit{fields}(\type{N}) = \overline{\type{U}\ f}$ by definition.
-%    $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$ by premise.
+    $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
 
-    $\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok$ %TODO
+    $\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[$\texttt{e}.\texttt{m}(\ol{e})$] 
@@ -152,10 +154,21 @@ $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
 % \end{description}
 % \end{lemma}
 
+\begin{lemma} \label{lemma:tvsNoFV}
+    \unify{} does not add free variables to types not containing free variables.
+    \begin{description}
+        \item[If] $(\sigma, \Delta) = \unify{} (C)$
+        \item[and] $\tv{a}$ being a type placeholders used in $C$
+        \item[then] $\text{fv}(\sigma(\tv{a})) = \emptyset$
+    \end{description}
+\end{lemma}
+\textit{Proof:}
+Trivial
+
 \begin{lemma} \label{lemma:unifyCC}
-Free variables do not leave their scope.
+Free variables do not leave their scope. TODO
 \begin{description}
-    \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdot \type{S} } } )$
+    \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdotCC \type{S} } } )$
     \item[and] $\text{fv}(\type{T}, \type{S}) \subseteq \text{fv}(\ol{T}, \ol{S})$, 
         $\sigma(\ol{T}) = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\type{T}) = \wcNtype{\Delta'}{N'}$
     \item[then] $ \Delta, \overline{\Delta}, \Delta' \vdash \sigma(\type{T}) <: \sigma(\type{S}) $
@@ -193,8 +206,8 @@ This rule is only applied for the outer wildcard environments for each type.
 
 % Problem: für tvs dürfen keine Wildcards eingesetzt werden, außer für die 
 
-\begin{lemma}
-The \unify{} algorithm only produces correct output for constraints not containing free variables.
+\begin{lemma}\label{lemma:unifySoundness}
+The \unify{} algorithm only produces correct output.
 \begin{description}
 \item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
 %\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$