diff --git a/prolog.tex b/prolog.tex
index 1ab89ef..988c762 100755
--- a/prolog.tex
+++ b/prolog.tex
@@ -1,5 +1,6 @@
 \usepackage{xspace}
 \usepackage{color,ulem}
+\usepackage{mathpartir}
 \usepackage{listings}
 \lstset{language=Java,
   showspaces=false,
diff --git a/soundness.tex b/soundness.tex
index 4fc6f90..7859104 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -91,6 +91,10 @@
 % TODO: 
 % \end{lemma}
 
+\unify{} calculates solutions for all normal type placeholders.
+Those are used for all untyped method's argument and return type.
+A correct typing for method calls can be deducted from those type informations.
+
 \begin{lemma}{Soundness:}\label{lemma:soundness}
     \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
     \begin{description}
@@ -131,7 +135,12 @@ 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[$\expr{v}.\texttt{f}$]
-        We are alowwed to use capture conversion for $\expr{v}$ here.
+    %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.
+    % can they contain free variables from other places? They could, but isolation prevents that.
+    % TODO: but how to proof?
+        We are allowed to use capture conversion for $\expr{v}$ here.
         $\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
         $\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and
         $\Delta \vdash \type{U}_i <: \sigma(\tv{a})$,
@@ -387,13 +396,20 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
 \unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
 \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[Then] there exists a substitution $\sigma'$ and a set of types $\overline{\wcNtype{\Delta}{N}}$ with:
-\begin{itemize}
-\item $\sigma \subseteq \sigma'$
-\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
-\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$ 
-\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
-\end{itemize}
+with $\text{wtv}(\ol{S}) = \emptyset$ and $\text{wtv}(\ol{T}) = \emptyset$
+\item[Then] $\Delta, \Delta' \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
+\item[and] either $\Delta, \Delta' \vdash \overline{\sigma(\type{S'}) <: \sigma(\type{T'})}$
+or $\Delta, \Delta', \overline{\Delta} \vdash \overline{\sigma'(\type{S'}) <: \sigma(\type{T'})}$
+with the capture converted substitution $\sigma' = \set{ \tv{a} \mapsto \type{N} \mid \tv{a} \mapsto \wcNtype{\Delta}{N} \in \sigma}$
+and $\overline{\Delta} = \set{\Delta \mid \tv{a} \mapsto \wcNtype{\Delta}{N} \in \sigma }$
+
+% there exists a substitution $\sigma'$ and a set of types $\overline{\wcNtype{\Delta}{N}}$ with:
+% \begin{itemize}
+% \item $\sigma \subseteq \sigma'$
+% \item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
+% \item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$ 
+% \item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
+% \end{itemize}
 \end{description}
 \end{lemma}
 
@@ -467,6 +483,13 @@ Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\ex
 <: \sigma'(\wctype{\Delta}{C}{\ol{T}})$ with $\overline{\Delta}$ being all the fresh wildcards generated by \rulename{Capture}.
 
 \item[Reduce]
+To proof $\wctype{\Delta}{C}{\ol{S}} <: \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{T}}$
+we have to show S-Exists for some $\Delta''$ and $\ol{T} = \sigma(\overline{\wtv{a}})$:
+\begin{itemize}
+\item $\Delta'' \vdash \subst{\ol{T}}{\ol{X}}\ol{L} <: \ol{T}$ by assumption and $\subst{\ol{\wtv{a}}}{\ol{X}}\ol{L} \lessdot \ol{\wtv{a}}$
+\item $\Delta'' \vdash \ol{T} <: \subst{\ol{T}}{\ol{X}}\ol{U}$ by assumption and $\ol{\wtv{a}} \lessdot \subst{\ol{\wtv{a}}}{\ol{X}}\ol{L}$
+\item $\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta'', \Delta')$ by setting $\Delta''$ accordingly
+\end{itemize}
 
 %Assumption and S-Exists.
 % Three different cases of the constraint $\exptype{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$:
diff --git a/unify.tex b/unify.tex
index f8f1dc8..adeba8b 100644
--- a/unify.tex
+++ b/unify.tex
@@ -576,18 +576,18 @@ gets the same wildcard twice.
                       \text{fv}(\type{T}) \subseteq \Delta', \, \text{wtv}(\type{T}) = \emptyset
                      \end{array}$\\
 \\
-      \rulename{Subst} &
-                       $\begin{array}[c]{l}
-  \wildcardEnv \vdash C \cup \set{\cctv{a} \doteq \wctype{\Delta}{C}{\ol{X}}}\\
-                         \hline
-  [\exptype{C}{\ol{X}}/\cctv{a}]\wildcardEnv \vdash [\exptype{C}{\ol{X}}/\cctv{a}]
-  C \cup \set{\ntv{a} \doteq \type{T}}
-                       \end{array}
-                     \quad \begin{array}{c}
-                      \ntv{a} \notin \wctype{\Delta}{C}{\ol{X}} \\
-                      \text{fv}(\wctype{\Delta}{C}{\ol{X}}) \subseteq \Delta', \, \text{wtv}(\wctype{\Delta}{C}{\ol{X}}) = \emptyset
-                     \end{array}$\\
-\\
+%       \rulename{Subst} &
+%                        $\begin{array}[c]{l}
+%   \wildcardEnv \vdash C \cup \set{\cctv{a} \doteq \wctype{\Delta}{C}{\ol{X}}}\\
+%                          \hline
+%   [\exptype{C}{\ol{X}}/\cctv{a}]\wildcardEnv \vdash [\exptype{C}{\ol{X}}/\cctv{a}]
+%   C \cup \set{\ntv{a} \doteq \type{T}}
+%                        \end{array}
+%                      \quad \begin{array}{c}
+%                       \ntv{a} \notin \wctype{\Delta}{C}{\ol{X}} \\
+%                       \text{fv}(\wctype{\Delta}{C}{\ol{X}}) \subseteq \Delta', \, \text{wtv}(\wctype{\Delta}{C}{\ol{X}}) = \emptyset
+%                      \end{array}$\\
+% \\
 \rulename{Subst-WC} &$
                 \begin{array}[c]{l}
 \wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{T}}\\
@@ -1019,6 +1019,53 @@ List<? extends Object> someList(){
 \caption{Constraint normalize rules}\label{fig:normalizing-rules}
 \end{figure}
 
+
+\begin{figure}
+\begin{mathpar}
+\inferrule[Capture]{
+        \wildcardEnv \vdash 
+        C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\ 
+}{
+      \wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}}
+        \vdash C \cup \, \set{  
+        [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
+} 
+      \quad \ol{\rwildcard{C}} \ \text{fresh}
+\and
+\inferrule[Reduce]{
+    \wildcardEnv \vdash 
+            C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot
+            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} }
+}{
+\wildcardEnv
+           \vdash C \cup \, \set{ 
+           \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
+          \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
+}
+\quad \text{wtv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
+\and
+\inferrule[Reduce-Empty]{
+    \wildcardEnv \vdash 
+            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
+            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} }
+}{
+\wildcardEnv
+           \vdash C \cup \, \set{ 
+           \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
+          \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
+}
+\and
+\inferrule[Exclude]{
+\wildcardEnv \vdash 
+C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} }
+}{
+\subst{\tv{a}}{\wtv{a}}\wildcardEnv \vdash 
+[\tv{a}/\wtv{a}]C \cup \, [\tv{a}/\wtv{a}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\  
+}\quad \Delta \neq \emptyset,
+\wtv{a} \in \text{fv}(\type{T}), \tv{a} \ \text{fresh}
+\end{mathpar}
+\end{figure}
+
 \begin{figure}
   \begin{center}
       \leavevmode