diff --git a/introduction.tex b/introduction.tex
index 22d7b28..4602610 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -18,7 +18,7 @@ List<String> ls = emptyList();
 Local type inference is based on matching and not unification \cite{javaTIisBroken}.
 When calling the \texttt{emptyList} method without context its return value will be set to a \texttt{List<Object>}.
 The following Java code snippet is incorrect, because \texttt{emptyList()} returns
-a \texttt{List<Object>} instead of the required \texttt{List<String>}.
+a \texttt{List<Object>} instead of the required \texttt{List<List<String>>}.
 \begin{verbatim}
 emptyList().add(new List<String>())
     .get(0)
@@ -40,8 +40,13 @@ this.<List<String>>emptyList().add(new List<String>())
     .get(0);
 \end{verbatim}
 
-%motivate constraints:
-For this example we will create constraints $\exptype{List}{\tv{a}} \lessdot \tv{b}...$ TODO
+%motivate constraints: 
+To solve this example we will create constraints
+$
+\exptype{List}{\tv{a}} \lessdot \tv{b},
+\tv{b} \lessdot \exptype{List}{\tv{c}},
+\tv{c} \lessdot \exptype{List}{\tv{d}}
+$ TODO
 Local type inference \cite{javaTIisBroken} is able to find a type substitution $\sigma$ satisfying
 $\overline{\type{A} <: \sigma(\type{F}) }, \sigma(\type{R}) <: \type{E}$.
 It is important that $\overline{\type{A}}$ and $\type{E}$ are given types and do not contain