diff --git a/paper/main.tex b/paper/main.tex
index 8362e44..fa7c4cb 100644
--- a/paper/main.tex
+++ b/paper/main.tex
@@ -176,11 +176,11 @@ $$\\$$
     \metavariable{x} \quad \valnonterm{\typevars}{\exprvars}
 }{Value Conactenation}
 
-%\otherform{
-%	\exprterminal{\Lambda} \metavariable{\alpha} \quad
-%	\exprterminal{\mapsto} \quad
-%	\valnonterm{ \typevars \cup \{ \metavariable{\alpha} \} }
-%}{Type-Function Value}
+\otherform{
+	\exprterminal{\Lambda} \metavariable{\alpha} \quad
+	\exprterminal{\mapsto} \quad
+	\valnonterm{ \typevars \cup \{ \metavariable{\alpha} \} }
+\{Type-Function Value}
 
 \otherform{
 	\exprterminal{\lambda} \metavariable{x} \quad
@@ -371,8 +371,8 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
 	}
 
 	\inferrule[T-TypeApp]{
-		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
-		\metavariable{\tau} \in \typenonterm{\typevars \cup \metavariable{\alpha}} \\
+		\metavariable{\tau} \in \typenonterm{\typevars \cup \{\metavariable{\alpha}\}} \\
+		\Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\
 		\metavariable{\sigma} \in \typenonterm{\typevars}
 	}{
 		\Gamma \vdash ( \metavariable{e} \quad \metavariable{\sigma} ) : \{\metavariable{\alpha} \mapsto \metavariable{\sigma}\} \metavariable{\tau}
@@ -520,42 +520,66 @@ which are given in \ref{def:evalrules}.
 
 
 \begin{lemma}[\(\beta\)-reduction preserves \(\delta\)-normalform]
-Assume \metavariable{e} is in \(\delta\)-normalform and \(\metavariable{e} \rightarrow \metavariable{e'}\). Then \(\metavariable{e'}\) is in \(\delta\)-normalform as well.
+\label{lemma:preserve-delta-normalform}
+Assume \metavariable{e} is in \(\delta\)-normalform and \(\metavariable{e} \rightarrow_\beta \metavariable{e'}\). Then \(\metavariable{e'}\) is in \(\delta\)-normalform as well.
 \begin{proof}
 \todo{}
 \end{proof}
 \end{lemma}
 
+\begin{lemma}[\(\delta\)-normalform eliminates compatibility]
+\label{lemma:eliminate-compat}
+Assume \(\emptyset \vdash \metavariable{e} :\approx \metavariable{\tau}\) and \(\metavariable{e} \rightarrow_{\delta}^* \metavariable{e'}\) such that \(\metavariable{e'}\) is in \(\delta\)-normalform.
+Then \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) 
+
+\begin{proof}
+\end{proof}
+
+\end{lemma}
+
 \subsection{Proof of Syntactic Type Soundness}
 
+\begin{lemma}[\(\beta\)-Preservation]
+\label{lemma:beta-preservation}
+Assume the expression \(\metavariable{e}\) is \textbf{syntactically well-typed}, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
+
+\begin{proof}
+\todo{}
+\end{proof}
+
+\end{lemma}
+
+\begin{lemma}[\(\delta\)-Preservation]
+\label{lemma:delta-preservation}
+
+\begin{proof}
+\todo{}
+\end{proof}
+\end{lemma}
+
+\begin{lemma}[Preservation]
+\label{lemma:preservation}
+Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
+
+\begin{proof}
+\todo{}
+\end{proof}
+\end{lemma}
+
 \begin{lemma}[Progress]
 \label{lemma:progress}
-
 If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\), then either \(\metavariable{e}\) is a value or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\)
 
 \begin{proof}
 \todo{}
 \end{proof}
-
 \end{lemma}
 
-
-\begin{lemma}[Preservation]
-\label{lemma:preservation}
-
-\begin{proof}
-\todo{}
-\end{proof}
-
-\end{lemma}
-
-
-
-
-\begin{theorem}[Type Soundness]
-If \(\emptyset \vdash \metavariable{e}:\metavariable{\tau}\), then it never occurs that \(\metavariable{e} \rightarrow_{eval}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
+\begin{theorem}[Soundness]
+If \(\emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\), then it never occurs that \(\metavariable{e} \rightarrow_{eval}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
 
 \begin{proof}
+By \ref{lemma:}
 Follows from \ref{lemma:progress} and \ref{lemma:preservation}.
 \end{proof}
 \end{theorem}