diff --git a/introduction.tex b/introduction.tex
index 5332f5e..22d7b28 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -15,15 +15,7 @@ because the expected return type is known. \texttt{List<String>} in this case.
 List<String> ls = emptyList();
 \end{lstlisting}
 
-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
-type placeholders already used in $\overline{\type{F}}$.
-
-The type parameters are not allowed on the left side of $A <: F$
-We can generate method calls where this is the case. The second call to \texttt{get}.
-
-Local type inference is based on matching and not unification.
+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>}.
@@ -36,87 +28,83 @@ emptyList().add(new List<String>())
 %List<A> <: List<B>, B <: List<C> 
 % B = A and therefore A on the left and right side of constraints.
 % this makes matching impossible
-
+The return type of the first \texttt{get} method is based on the return type of
+\texttt{emptyList},
+but the second call to \texttt{get} is only possible if \texttt{emptyList} returns
+a list of lists.
+The local type inference algorithm based on matching cannot produce this solution.
+Here a type inference algorithm based on unification is needed.
 \begin{verbatim}
 this.<List<String>>emptyList().add(new List<String>())
     .get(0)
     .get(0);
 \end{verbatim}
 
-Local type inference cannot deal with type inference during the algorithm.
-If the left side contains unknown type parameters.
+%motivate constraints:
+For this example we will create constraints $\exptype{List}{\tv{a}} \lessdot \tv{b}...$ 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
+type placeholders already used in $\overline{\type{F}}$.
+
+The type parameters are not allowed on the left side of $A <: F$
+We can generate method calls where this is the case. The second call to \texttt{get}.
+
+% Local type inference cannot deal with type inference during the algorithm.
+% If the left side contains unknown type parameters.
 
 
-\begin{verbatim}
-import java.util.ArrayList;
-import java.util.stream.*;
+% \begin{verbatim}
+% import java.util.ArrayList;
+% import java.util.stream.*;
 
-class Test {
-    void test(){
-        var s = new ArrayList<String>().stream().map(i -> 1);
-        receive(s);
-    }
+% class Test {
+%     void test(){
+%         var s = new ArrayList<String>().stream().map(i -> 1);
+%         receive(s);
+%     }
 
-    void receive(Stream<Object> l){}
-}
-\end{verbatim}
+%     void receive(Stream<Object> l){}
+% }
+% \end{verbatim}
 
-TypeError:
-\begin{verbatim}
-void test(){
-        var l = new ArrayList<String>();
-        l.add("hi");
-        var  s = l.stream().map(i -> 1).collect(Collectors.toList());
-        var s2 = l.stream().map(i -> "String").collect(Collectors.toList());
-        receive(s, s2);
-    }
-    <A> void receive(List<A> l, List<A> l2){}
-\end{verbatim}
-Correct:
-\begin{verbatim}
-void test(){
-        var l = new ArrayList<String>();
-        l.add("hi");
-        List<Object>  s = l.stream().map(i -> 1).collect(Collectors.toList());
-        List<Object> s2 = l.stream().map(i -> "String").collect(Collectors.toList());
-        receive(s, s2);
-    }
-    <A> void receive(List<A> l, List<A> l2){}
-\end{verbatim}
-
-Error:
-\begin{verbatim}
-rrr(this.emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
-\end{verbatim}
-Correct:
-\begin{verbatim}
-rrr(this.<Box<?>>emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
-\end{verbatim}
-
-incorrect:
-\begin{verbatim}
-emptyList().add(emptyList()).head().head()
-\end{verbatim}
-
-In this example the return type of \texttt{emptyList} needs to consider that it should contain a list of a list.
-This is a limitation of local type inference as presented here \cite{javaTIisBroken}.
+% TypeError:
+% \begin{verbatim}
+% void test(){
+%         var l = new ArrayList<String>();
+%         l.add("hi");
+%         var  s = l.stream().map(i -> 1).collect(Collectors.toList());
+%         var s2 = l.stream().map(i -> "String").collect(Collectors.toList());
+%         receive(s, s2);
+%     }
+%     <A> void receive(List<A> l, List<A> l2){}
+% \end{verbatim}
+% Correct:
+% \begin{verbatim}
+% void test(){
+%         var l = new ArrayList<String>();
+%         l.add("hi");
+%         List<Object>  s = l.stream().map(i -> 1).collect(Collectors.toList());
+%         List<Object> s2 = l.stream().map(i -> "String").collect(Collectors.toList());
+%         receive(s, s2);
+%     }
+%     <A> void receive(List<A> l, List<A> l2){}
+% \end{verbatim}
 
+% Error:
+% \begin{verbatim}
+% rrr(this.emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
+% \end{verbatim}
+% Correct:
+% \begin{verbatim}
+% rrr(this.<Box<?>>emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
+% \end{verbatim}
 
 % \begin{recap}{Java Local Type Inference}
 % Local type inference is able to solve constraints of the form 
 % T <. b, b <. T where T are given types
 % \end{recap}
 % Local Type inference cannot infer F-Bounded types (TODO: we can, right?)
-The big difference to local type inference is the ability to have constraints where both sides contain type placeholders.
-As described in \cite{javaTIisBroken} local type inference is able to determine an unifier $\sigma$
-which satisfies $\set{\overline{A <: \sigma(F)}, \sigma(R) <: E }$.
-Note that $A$ and $E$ are already given types.
-$A$ are method arguments and $E$ is the expected return type.
-
-% Are there examples where the expected return type is not given?
-% with global type inference this is easy to produce
-% an example where this is the case for local type inference?
-%   - the val example
 
 \section{Type Inference for Java}
 %The goal is to find a correct typing for a given Java program.