diff --git a/soundness.tex b/soundness.tex
index 63d7571..e8aa7fc 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -97,28 +97,29 @@ By structural induction over the expression $\texttt{e}$.
 
     \item[$\texttt{e}.\texttt{m}(\ol{e})$]
 Lets have a look at the case where the receiver and parameter types are all named types.
-So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta'}{N}$:
-    \begin{gather}
+So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta'}{N}$:    
+\begin{gather}
+        \label{sp:0}
+        \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\
         \label{sp:1}
         \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
         \label{sp:2}
         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
+        \label{sp:3}
         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
         \label{sp:4}
         \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
     \end{gather}
-    \ref{sp:1} is guaranteed by the constraints $\ol{r} \lessdot \ol{T}$.
-    $\ol{\tv{r}} \lessdot \ol{T}$ says that there is a $\Delta'$ with 
-    $\Delta, \Delta' \vdash CC(\sigma(\tv{r})) <: \type{T}$.
+    \ref{sp:0}, \ref{sp:1} and \ref{sp:2} are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness} and \ref{lemma:unifyCC}.
+    \ref{sp:4} due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
+    $\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
+    $\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
+    therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
+    by lemma \ref{lemma:wfHereditary} and \ref{sp:3} by premise of WF-Class.
+    The same goes for $\wcNtype{\Delta'}{N}$.
+    $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ TODO!
 
-    If $\overline{\sigma(\tv{r}) = \wcNtype{\Delta}{N}}$
-    then \ref{sp:1} due to lemma \ref{lemma:unifyCC}.
-    Let $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$, then
-    \ref{sp:4} by lemma \ref{lemma:unifySoundness} and \ref{lemma:tvsNoFV}.
-    The environments $\overline{\Delta}$ are not needed,
-    because none of the variables in $\text{dom}(\overline{\Delta})$ are used in $\ol{T}$ or $\Delta, \Delta'$.
-
-\ref{sp:3}
+%\ref{sp:3}
 %TODO: S is not in \sigma. They are generated by a local type inference algorithm
 
 Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
@@ -154,22 +155,30 @@ Method calls generate multiple constraints that share the same wildcard placehol
 % $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
 % %UNIFY fails when there are free variables on the right side of a a =. T constraint
 
-\begin{lemma}
+\begin{lemma}\label{lemma:unifyWellFormedness}
 \unify{} generates well-formed types as long as well-formed types are supplied.
 \begin{description}
-\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$ and $\sigma(\tv{a}) = \wcNtype{\ol{\wildcard{X}{\type{U}}{\type{L}}}}{N}$
-\item[and] $\forall \wcNtype{\Delta}{N} \in C: \ \Delta' \vdash \wcNtype{\Delta}{N} \ \ok$ 
-\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
+\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$ %and $\sigma(\tv{a}) = \wcNtype{\ol{\wildcard{X}{\type{U}}{\type{L}}}}{N}$
+\item[and] $\wcNtype{\Delta}{N} \in C \implies \Delta' \vdash \wcNtype{\Delta}{N} \ \ok$ 
+%\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
+\item[then] $\Delta \vdash \sigma(\tv{a}) \ \ok$
 \end{description}
 \end{lemma}
-Only the \rulename{General} rule generates fresh wildcards.
-By lemma \ref{lemma:unifySoundness} we get $\Delta \vdash \sigma(\type{T}) <: \sigma(\tv{a})$ with $\sigma(\tv{a}) = \wctype{\ol{\wildcard{X}{\sigma(U)}{\sigma(L)}}}{C}{\ol{X}}$
-By S-Exists and S-Trans we can say $\Delta \vdash \sigma(\type{L}) <: \sigma(\type{U})$
+%Only the \rulename{General} rule generates fresh wildcards.
+%By lemma \ref{lemma:unifySoundness} we get $\Delta \vdash \sigma(\type{T}) <: \sigma(\tv{a})$ with $\sigma(\tv{a}) = \wctype{\ol{\wildcard{X}{\sigma(U)}{\sigma(L)}}}{C}{\ol{X}}$
+%By S-Exists and S-Trans we can say $\Delta \vdash \sigma(\type{L}) <: \sigma(\type{U})$
+\textit{Proof:}
+by induction over every step of the \unify{} algorithm.
+Hint: a type placeholder $\tv{a}$ will never be replaced by a free variable or a type containing free variables.
+This fact together with the presumption that every supplied type is well-formed we can easily show that this lemma is true.
+
+\textit{Proof: (Variant 2)}
+The GenSigma and GenDelta rules check for well-formedness.
 
 % All types supplied to the Unify algorithm by TYPEs only contain ? extends or ? super wildcards. (X : [bot..T] or X : [T .. Object]).
 % Both are well formed!
 
-\begin{lemma}
+\begin{lemma}\label{lemma:wfHereditary}
     Well-formedness is hereditary
     \begin{description}
         \item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$