diff --git a/Vorlesungen/ThProg/Konfluenz.tex b/Vorlesungen/ThProg/Konfluenz.tex
index bc24bcd..58f0f1c 100644
--- a/Vorlesungen/ThProg/Konfluenz.tex
+++ b/Vorlesungen/ThProg/Konfluenz.tex
@@ -9,7 +9,8 @@
 	\section*{Wichtige Lemmas}
 		\subsection*{Newman's Lemma:}
 			Ein stark normalisierendes und lokal Konfluentes Termersetzungssystem (TES) ist konfluent.
-		\subsection*{}
+		\subsection*{Critical Pair Lemma:}
+			Ein TES ist lokal konfluent, wenn alle kritischen Paare zusammenf\"uhrbar sind.
 		\section{Matching Table:}
 			Formeln:
 			\begin{align}
diff --git a/Vorlesungen/ThProg/Strukturelle_Induktion.tex b/Vorlesungen/ThProg/Strukturelle_Induktion.tex
index 4f30a87..0799033 100644
--- a/Vorlesungen/ThProg/Strukturelle_Induktion.tex
+++ b/Vorlesungen/ThProg/Strukturelle_Induktion.tex
@@ -37,7 +37,7 @@
 	\[as+(Cons\;e\;ys) = (snoc\;as\;e)+ys\]
 \newpage
 	\textbf{Induktionsschritt (IS):}\\\\
-	$as\;=\;Cons\;a\;as$\\$\Rightarrow$ Einsetzen und wieder beide Seiten maximal vereinfachen,auf einer Seite die Induktionshypothese reinfrikeln (idR. nur auf einer Seite,z.B. auf der linken)
+	$xs\;=\;Cons\;a\;as$\\$\Rightarrow$ Einsetzen und wieder beide Seiten maximal vereinfachen,auf einer Seite die Induktionshypothese reinfrikeln (idR. nur auf einer Seite,z.B. auf der linken)
 	\begin{align*}
 		Cons\;a\;as\;+(Cons\;e\;ys)\;&=\;snoc\;((Cons\;a\;as)\;e)+ys \\
 		Cons\;a\;(\underbrace{as\;+(Cons\;e\;ys)}_{IH\;links})\;&=\;snoc\;((Cons\;a\;as)\;e)+ys\\
diff --git a/Vorlesungen/ThProg/SystemF.tex b/Vorlesungen/ThProg/SystemF.tex
index 30085e7..e5245ac 100644
--- a/Vorlesungen/ThProg/SystemF.tex
+++ b/Vorlesungen/ThProg/SystemF.tex
@@ -86,9 +86,9 @@
 		$(5)\;
 			\Gamma \;\cup \{\,n:\mathrm{N}\,\} \vdash
 			\overbrace{
-			n\,:\,(\,a\,\rightarrow\,a\,)\rightarrow (\,a\,\rightarrow \,a\,)
+			n\,:\,\forall a\,.',(\,a\,\rightarrow\,a\,)\rightarrow (\,a\,\rightarrow \,a\,)
 			}^{per\;Definition\; =\;\mathrm{N}}
-			\hspace{1cm}
+			\hspace{8mm}
 			\overbrace{
 			mult:\;\mathrm{N}\rightarrow \mathrm{N}\rightarrow \mathrm{N}
 			}^{Ax}
@@ -104,7 +104,7 @@
 			\Gamma \;\cup \{\,n:\mathrm{N}\,\} \vdash 
 			n\,:\,(\,\mathrm{N}\rightarrow \mathrm{N}\,)
 			\rightarrow (\,\mathrm{N}\rightarrow \mathrm{N}\,)
-			\hspace{2cm}
+			\hspace{25mm}
 			mult\;two\;\mathrm{N}\rightarrow \mathrm{N}
 		$
 	}\\
@@ -136,22 +136,11 @@
 	$		
 	\\
 	\textbf{Erkl\"arungen:}\\
-	\begin{small}
-	- (1) $\rightarrow_{i}$\\
-	- (2)(3) $\rightarrow_e$\\
-	- in (3) ist $[\,one:\mathrm{N}\,]$ mit Ax fertig\\
-	- in (4) $\forall _e$\\
-	- (4)(links) $\forall_{e}$ (rechts) $\rightarrow_e$\\
-	\end{small}	
-	\\
+	(1) $\rightarrow_{i}$\\
+	(2)(3) $\rightarrow_e$\\
+	(3)(rechts)$[\,one:\mathrm{N}\,]$ mit Ax fertig\\
+	(4) $\forall _e$ (wir wissen, dass N : $(a->a)->a->a$ ist, und dass \{n : N ist\}; damit n hinten also mit dem Kontex aufgeht muss es von der Form $(a->a)->a->a$ sein)\\
+	(4)(links) $\forall_{e}$ (rechts) $\rightarrow_e$\\\\
 	\textbf{Eine \"Ubersicht der Regeln findet sich in den \"Ubungsfolien oder dem SS14 Spickzettel!}
-		
-		
-		
-		
-		
-$ $\\\\
-\begin{tiny}
-	\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
-\end{tiny}
+	
 \end{document}
\ No newline at end of file