diff --git a/slides/ThProgUE9.pdf b/slides/ThProgUE9.pdf
new file mode 100644
index 0000000..609a684
Binary files /dev/null and b/slides/ThProgUE9.pdf differ
diff --git a/slides09.tex b/texfiles/slides09.tex
similarity index 92%
rename from slides09.tex
rename to texfiles/slides09.tex
index be17d94..3d9d0a5 100644
--- a/slides09.tex
+++ b/texfiles/slides09.tex
@@ -206,8 +206,14 @@ Leon Vatthauer}
 % Introduction
 \section{Aufgabe 1 - Beweise mittels struktureller Induktion}
 \begin{frame}[t, fragile]{Aufgabe 1}{Beweise mittels struktureller Induktion}
-    Wir betrachten die folgenden Funktionen auf Listen:
-
+    Wir betrachten erneut den Datentyp der Listen sowie die folgenden Funktionen:
+    \begin{minipage}{.45\textwidth}
+        \begin{lstlisting}[keywords={data, where, List, Nat}]
+data List a where
+    Nil  : () $\rightarrow$ List a
+    Cons : a $\rightarrow$ List a $\rightarrow$ List a
+        \end{lstlisting}
+    \end{minipage}
     \begin{minipage}{.45\textwidth}
         \begin{lstlisting}[keywords={List, Nat}]
 length : List a $\rightarrow$ Nat
@@ -222,7 +228,7 @@ reverse Nil = Nil
 reverse (Cons x xs) = snoc (reverse xs) x
         \end{lstlisting}
     \end{minipage}
-    \begin{minipage}{.5\textwidth}
+    \begin{minipage}{.45\textwidth}
         \begin{lstlisting}[keywords={List, Nat}]
 snoc : List a $\rightarrow$ List a
 snoc Nil y = Cons y Nil
@@ -238,8 +244,14 @@ snoc (Cons x xs) y = Cons x (snoc xs y)
 \end{frame}
 
 \begin{frame}[t, fragile]{Aufgabe 1}{Beweise mittels struktureller Induktion}
-    Wir betrachten die folgenden Funktionen auf Listen:
-
+    Wir betrachten erneut den Datentyp der Listen sowie die folgenden Funktionen:
+    \begin{minipage}{.45\textwidth}
+        \begin{lstlisting}[keywords={data, where, List, Nat}]
+data List a where
+    Nil  : () $\rightarrow$ List a
+    Cons : a $\rightarrow$ List a $\rightarrow$ List a
+        \end{lstlisting}
+    \end{minipage}
     \begin{minipage}{.45\textwidth}
         \begin{lstlisting}[keywords={List, Nat}]
 length : List a $\rightarrow$ Nat
@@ -254,7 +266,7 @@ reverse Nil = Nil
 reverse (Cons x xs) = snoc (reverse xs) x
         \end{lstlisting}
     \end{minipage}
-    \begin{minipage}{.5\textwidth}
+    \begin{minipage}{.45\textwidth}
         \begin{lstlisting}[keywords={List, Nat}]
 snoc : List a $\rightarrow$ List a
 snoc Nil y = Cons y Nil
@@ -308,13 +320,13 @@ size (Inner x l r) = 1 + size l + size r
     \end{minipage}
     \vfill
     Definieren Sie induktiv eine Funktion \lstinline[keywords={List, Tree}]{inorder : Tree a $\rightarrow$ List a}, die die Elemente eines Baumes
-    gemäß ener In-Order-Traversierung von links nach rechts ausgibt. Zeigen Sie dann per struktureller Induktion über Bäume, dass
+    gemäß einer In-Order-Traversierung von links nach rechts ausgibt. Zeigen Sie dann per struktureller Induktion über Bäume, dass
     $$\forall\texttt{t. length (inorder t) = size t}$$
 \end{frame}
 \begin{frame}[t, fragile]{Aufgabe 3.2}{Induktion über Bäume}
     Wir betrachten im folgenden einen parametrischen induktiven Datentyp für Bäume, deren Blätter Elemente vom Typ $a$ enthalten, und deren innere Knoten jeweils
     bis zu drei Kinder haben, selbst aber keine Werte enthalten:
-    \begin{lstlisting}[keywords={VarTree}]
+    \begin{lstlisting}[keywords={VarTree, data, where}]
 data VarTree a where
     VLeaf : a $\rightarrow$ VarTree a
     Node1 : VarTree a $\rightarrow$ VarTree a