diff --git a/introduction.tex b/introduction.tex
index 20226ea..39c22ab 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -584,14 +584,23 @@ compare(p); // Error
 
 Our type inference algorithm is not able to solve this example.
 When we convert this to \TamedFJ{} and generate constraints we end up with:
-%TODO: Finish this example! does it work?
 \begin{lstlisting}[style=tamedfj]
-let x = l in let m = make(x) in compare(m)
+let m = let x = l in make(x) in compare(m)
 \end{lstlisting}
-\begin{constraints}
+\begin{constraintset}$
+\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
+\ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
+\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
+\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
+$\end{constraintset}
 
-\end{constraints}
+$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
+from the constraint
+$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
+\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to 
+$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.
 
+Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
 %TODO
 
 \begin{lstlisting}[style=letfj]