diff --git a/introduction.tex b/introduction.tex
index 1436b9e..f3d9515 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -4,6 +4,21 @@
 % - Kapitel 1.2 + 1.3 ist noch zu komplex
 % - Constraints und Unifikation erklären, bevor Unifikation erwähnt wird
 
+\section{Motivation}
+\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);
+    }
+
+    void receive(Stream<Object> l){}
+}
+\end{verbatim}
+
 \section{Type Inference for Java}
 %The goal is to find a correct typing for a given Java program.
 Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them,
diff --git a/todo-11.4.24 b/todo-11.4.24
index 1c13620..fe6fd85 100644
--- a/todo-11.4.24
+++ b/todo-11.4.24
@@ -2,6 +2,7 @@
 - Motivation (gibt es ein nicht funktionierendes Beispiel für lokale Typinferenz was mit unserem algorithmus funktioniert)
 - Zeile 52 steht LetFJ, muss eingeführt werden
 	- Operatoren motivieren. Denotable expressable types
+	Java macht CC implizit. Wir machen es mit let statements. Dadurch LetFJ einführen
 	- Java macht es anders. es gibt keine let statements
 	- In java kann ich die lets nur in bestimmter Weise einbauen. Die ANF Transformation macht aus TamedFJ das letFJ