diff --git a/introduction.tex b/introduction.tex
index fd838f6..72e17bf 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -287,10 +287,10 @@ $\begin{array}{c}
 \wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
 \\
 \hline
-\textit{Capture Conversion:}\ \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
+\textit{Capture Conversion:}\ \wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
 \\
 \hline
-\textit{Solution:}\ \wtv{a} \doteq \rwildcard{X} \implies \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\rwildcard{X}}, \, \type{String} \lessdot \rwildcard{X}
+\textit{Solution:}\ \wtv{a} \doteq \rwildcard{Y} \implies \wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}, \, \type{String} \lessdot \rwildcard{Y}
 \end{array}
 $
 \end{center}
@@ -304,7 +304,11 @@ which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X
 The type of \texttt{l} can be capture converted by a let statement if needed (see listing \ref{lst:addExampleLet}).
 Therefore we assign the constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
 which allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
-\textit{Note:} The constraint $\type{String} \lessdot \rwildcard{X}$ is satisfied because $\rwildcard{X}$ has $\type{String}$ as lower bound.
+The captured wildcard $\rwildcard{X}$ gets a fresh name and is stored in the wildcard environment of the \unify{} algorithm.
+
+
+\textit{Note:} The constraint $\type{String} \lessdot \rwildcard{Y}$ is satisfied
+because $\rwildcard{Y}$ has $\type{String}$ as lower bound.
 
 
 For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
@@ -695,4 +699,12 @@ But afterwards a capture conversion is applied, which can generate different typ
 \begin{itemize}
   \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$ 
   \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$ 
-\end{itemize}
\ No newline at end of file
+\end{itemize}
+
+Wildcards are not reflexive. A box of type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$
+is able to hold a value of any type. It could be a $\exptype{Box}{String}$ or a $\exptype{Box}{Integer}$ etc.
+Also two of those boxes do not necessarily contain the same type.
+But there are situations where it is possible to assume that.
+For example the type $\wctype{\rwildcard{X}}{Pair}{\exptype{Box}{\rwildcard{X}}, \exptype{Box}{\rwildcard{X}}}$
+is a pair of two boxes, which always contain the same type.
+Inside the scope of the \texttt{Pair} type, the wildcard $\rwildcard{X}$ stays the same.
\ No newline at end of file
diff --git a/prolog.tex b/prolog.tex
index 27135fa..4986283 100755
--- a/prolog.tex
+++ b/prolog.tex
@@ -20,6 +20,7 @@
 
 \newcommand{\tifj}{\texttt{TamedFJ}}
 
+\newcommand{\wcSep}{\vdash}
 \newcommand\mv[1]{{\tt #1}}
 \newcommand{\ol}[1]{\overline{\tt #1}}
 \newcommand{\exptype}[2]{\mathtt{#1 \texttt{<} #2 \texttt{>} }}