diff --git a/paper/main.tex b/paper/main.tex
index 3577d3c..1073bc8 100644
--- a/paper/main.tex
+++ b/paper/main.tex
@@ -508,40 +508,42 @@ while preserving its semantics.
 
 \subsubsection{Inference of Expression Types}
 
-The type-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\) is a finite mapping from variables \(\metavariable{x_i} \in \exprvars\) to ground types \(\metavariable{\tau_i} \in \typenonterm{\emptyset}\).
+As usual, the typing-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\)
+is a finite mapping which assigns variables \(\metavariable{x_i} \in \exprvars\) to types \(\metavariable{\tau_i} \in \nonterm{T}\).
 Using the inference rules given in \ref{def:typerules}, further typing-judgements
 of the form
 \begin{itemize}
-\item \(\metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" and
-\item \(\metavariable{e} :\approx \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is compatible with type \(\metavariable{\tau}\)"
+\item \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" and
+\item \(\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is compatible with type \(\metavariable{\tau}\)"
 \end{itemize}
-can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \exprnonterm{\emptyset}{\exprvars}\) and \(\metavariable{\tau} \in \typenonterm{\emptyset}\)
+can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
+
+
 
 \begin{definition}[Syntactic Well-Typedness]
-An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
+An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
 such that \( \emptyset \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}.
 \end{definition}
 
 \begin{definition}[Semantic Well-Typedness]
-An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
-such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules}.
+An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
+such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules} and \ref{def:semtyperules}.
 \end{definition}
 
-\begin{definition}[Inference Rules for the Typing Relation.]
-  \label{def:typerules}
 
-As usual, each rule is composed of premises (above the horizontal line) and a conclusion (below the line):
+\begin{definition}[Syntactic Typing Relation]
+
+\label{def:typerules}
 \begin{mathpar}
 
 	\inferrule[T-Variable]{
-		\metavariable{x} \in \exprvars\\
-		\metavariable{\tau} \in \nonterm{T}\\
+%		\metavariable{x} \in \exprvars\\
+%		\metavariable{\tau} \in \nonterm{T}\\
 		\metavariable{x}:\metavariable{\tau} \in \Gamma\\
 	}{
 		\Gamma \vdash \metavariable{x}:\metavariable{\tau}
 	}\and
 
-
 	\inferrule[T-LetBinding]{
 		\Gamma \vdash \metavariable{e} : \metavariable{\sigma} \\
 		\Gamma , \metavariable{x}:\metavariable{\sigma} \vdash \metavariable{t} : \metavariable{\tau}
@@ -549,17 +551,16 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
 		\Gamma \vdash (\exprterminal{\text{let }}\metavariable{x}\exprterminal{\text{ = }}\metavariable{e}\exprterminal{\text{ in }} \metavariable{t}) : \metavariable{\tau}
 	}
 
-
 	\inferrule[T-TypeAbs]{
-		\metavariable{\tau} \in \nonterm{T} \\
-		\metavariable{e} \in \nonterm{E} \\
+%		\metavariable{\tau} \in \nonterm{T} \\
+%		\metavariable{e} \in \nonterm{E} \\
 		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
 	}{
         \Gamma \vdash (\exprterminal{\Lambda} \metavariable{\alpha} \exprterminal{\mapsto} \metavariable{e}) : \typeterminal{\forall}\metavariable{\alpha}\typeterminal{.}\metavariable{\tau}
 	}
 
 	\inferrule[T-TypeApp]{
-		\metavariable{\tau} \in \nonterm{T} \\
+%		\metavariable{\tau} \in \nonterm{T} \\
 		\Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\
 		\metavariable{\sigma} \in \nonterm{T}
 	}{
@@ -567,42 +568,34 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
 	}
 
 
-	\inferrule[T-ValueAbs]{
-		\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
-		\metavariable{e} \in \nonterm{E} \\
-		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
+	\inferrule[T-Abs]{
+%		\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
+%		\metavariable{e} \in \nonterm{E} \\
+		\Gamma,\metavariable{x}:\metavariable{\sigma} \vdash \metavariable{e} : \metavariable{\tau} \\
 	}{
         \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\sigma} \exprterminal{\mapsto} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
 	}
 
-	\inferrule[T-ValueApp]{
+	\inferrule[T-App]{
 		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau} \\
 		\Gamma \vdash \metavariable{a} : \metavariable{\sigma} \\
 	}{
 		\Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau}
 	}\and
 
-
-	\inferrule[T-Compatible]{
-		\Gamma \vdash \metavariable{e} : \metavariable{\tau}
-	}{
-		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}
-	}\and
-	
 	\inferrule[T-MorphAbs]{
-		\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
-		\metavariable{e} \in \nonterm{E} \\
-		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
-	}{
-        \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
-	}\and
-
-	\inferrule[T-MorphApp]{
-		\Gamma \vdash \metavariable{e} : \metavariable{\tau}\\
-		\exists \metavariable{h} . \Gamma \vdash \metavariable{h} : \metavariable{\tau} \typeterminal{\rightarrow_{morph}} \metavariable{\tau'}\\
+%		\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
+%		\metavariable{e} \in \nonterm{E} \\
+		\Gamma,\metavariable{x}:\metavariable{\tau} \vdash \metavariable{e} : \metavariable{\tau'} \\
 		\metavariable{\tau} \precsim \metavariable{\tau'}
 	}{
-		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
+        \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\tau}\typeterminal{\rightarrow_{morph}}\metavariable{\tau'}
+	}\and
+
+	\inferrule[T-MorphFun]{
+        \Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
+	}{
+        \Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
 	}\and
 
 	\inferrule[T-Ascension]{
@@ -617,16 +610,98 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
 		\metavariable{\tau} \leq \metavariable{\tau'}
 	}{
 		\Gamma \vdash \metavariable{e} : \metavariable{\tau'}
-	}\and
+	}
 
 \end{mathpar}
 \end{definition}
 
+\begin{definition}[Semantic Typing Relation]
+\label{def:semtyperules}
+\begin{mathpar}
+	\inferrule[T-NativeRepr]{
+		\Gamma\vdash \metavariable{e} : \metavariable{\tau}
+	}{
+		\Gamma\vdash \metavariable{e} :\approx \metavariable{\tau}
+	}
+
+	\inferrule[T-CoercedRepr]{
+		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}\\
+%		\metavariable{\tau} \precsim \metavariable{\tau'}\\
+		%\exists \metavariable{h} \text{ s.t. }
+		\Gamma \vdash \metavariable{h}: \typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}}
+	}{
+		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
+	}
+
+
+	\inferrule[T-CompatibleApp]{
+		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \rightarrow \metavariable{\tau}\\
+		\Gamma \vdash \metavariable{a} :\approx \metavariable{\sigma}
+	}{
+		\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau}
+	}
+\end{mathpar}
+\end{definition}
+
+\subsection{Coercion Semantics}
+
+We define the translation function \(\llbracket . \rrbracket\) which completes a \emph{semantically well-typed} expression
+by inserting all required coercions based on the typing derivation of the expression.
+The result shall be a \emph{syntactically well-typed} expression.
+
+We write \(C :: \sigma \precsim \tau\) to mean "C is a subtyping derivation tree whose conclusion is \(\sigma \precsim \tau\)".
+Similarly, we write \(D :: \Gamma \vdash e : \tau\) to mean "D is a typing derivation whose conclusion is \(\Gamma \vdash e : \tau\)"
+
+\begin{definition}[Translation]
+\begin{mathpar}
+
+\Big{\llbracket} \inferrule[T-SemanticSubtype]{
+	D_1 :: \Gamma \vdash \metavariable{h}:\metavariable{\tau} \typeterminal{\rightarrow_\text{morph}} \metavariable{\tau'}\\
+    D_2 :: \Gamma \vdash \metavariable{e}:\metavariable{\tau}\\
+%	C :: \metavariable{\tau} \precsim \metavariable{\tau'}
+}{
+	\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
+}\Big{\rrbracket} = \exprterminal{(}
+\llbracket D_1 \rrbracket \llbracket D_2 \rrbracket
+%\metavariable{h} \llbracket D_2 \rrbracket
+\exprterminal{)}
+
+\Big{\llbracket} \inferrule[T-CoercedApp]{
+	D_1 :: \Gamma \vdash \metavariable{f}:\metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
+    D_2 :: \Gamma \vdash \metavariable{a}:\approx\metavariable{\sigma}
+}{
+	\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau}
+}\Big{\rrbracket} = \exprterminal{(}
+%\exprterminal{(}\metavariable{f} \llbracket D_2 \rrbracket \exprterminal{)}
+\llbracket D_1 \rrbracket \llbracket D_2 \rrbracket
+\exprterminal{)}
+
+\Big{\llbracket}
+\inferrule[\emph{Otherwise}]{}{
+D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}
+}
+\Big{\rrbracket} = \metavariable{e}
+
+\end{mathpar}
+\end{definition}
+
+\begin{lemma}[Elimination of \(:\approx\)]
+\label{lemma:translation}
+
+For all \emph{semantically well-typed} expressions \metavariable{e} with the typing derivation \(D :: \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau}\),
+the translation \(\llbracket D \rrbracket = \metavariable{e'}\), yields a \emph{syntactically well-typed} expression \metavariable{e'} with
+\(\emptyset \vdash \metavariable{e'} : \metavariable{\tau} \)
+
+\begin{proof}
+\todo{}
+\end{proof}
+
+\end{lemma}
+
 
 \subsection{Evaluation}
 
-Evaluation of an expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is defined by exhaustive application of the rewrite rules \(\rightarrow_\beta\) and \(\rightarrow_\delta\),
-which are given in \ref{def:evalrules}.
+Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by exhaustive application of the rewrite rule \(\rightarrow_\beta\) as in \ref{def:evalrules}.
 
 \begin{definition}[Inference Rules for Evaluation]
 \label{def:evalrules}
@@ -644,13 +719,13 @@ which are given in \ref{def:evalrules}.
 	\inferrule[E-App2]{
 		\metavariable{e_2} \rightarrow_\beta \metavariable{e_2'}
 	}{
-		\metavariable{e_1} \metavariable{e_2}
+		\metavariable{v_1} \metavariable{e_2}
 		\rightarrow_\beta
-		\metavariable{e_1} \metavariable{e_2'}
-	}
+		\metavariable{v_1} \metavariable{e_2'}
+	}\and
 
 	\inferrule[E-TypApp]{
-		\metavariable{\tau} \in \typenonterm{\emptyset}\\
+%		\metavariable{\tau} \in \typenonterm{\emptyset}\\
 		\metavariable{e} \rightarrow_\beta \metavariable{e'}
 	}{
 		\metavariable{e}
@@ -671,7 +746,6 @@ which are given in \ref{def:evalrules}.
 		\rightarrow_\beta
 		\{ \metavariable{\alpha} \mapsto \metavariable{\tau} \} \metavariable{e}
 	}\and
-
 	\inferrule[E-AppLam]{
 	}{
 		\exprterminal{(\lambda} \metavariable{x}
@@ -690,64 +764,27 @@ which are given in \ref{def:evalrules}.
 		\exprterminal{\text{ in }}\metavariable{e}
 		\rightarrow_\beta
 		\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
-	}
-
-
-	\inferrule[E-ImplicitCast]{
-		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau} \\
-		\Gamma \vdash \metavariable{h} : \metavariable{\sigma'} \typeterminal{\rightarrow_{morph}} \metavariable{\sigma} \\
-		\Gamma \vdash \metavariable{a} : \metavariable{\sigma'}
+	}\and
+	\inferrule[E-Ascribe]{
 	}{
-		\exprterminal{(} \metavariable{f} \quad \metavariable{a} \exprterminal{)}
-		\rightarrow_\delta
-		\exprterminal{(} \metavariable{f} \quad \exprterminal{(} \metavariable{h} \quad \metavariable{a} \exprterminal{))}
+		\metavariable{e}
+		\exprterminal{\text{ as }}
+		\metavariable{\tau}
+		\rightarrow_\beta
+		\metavariable{e}
 	}
-
 \end{mathpar}
 \end{definition}
 
 
-\begin{lemma}[\(\beta\)-reduction preserves \(\delta\)-normalform]
-\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{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.
+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_{\beta} \metavariable{e'}\)
+it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
 
 \begin{proof}
 \todo{}
@@ -756,23 +793,44 @@ Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdas
 
 \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'}\)
+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_{\beta} \metavariable{e'}\)
 
 \begin{proof}
 \todo{}
 \end{proof}
 \end{lemma}
 
-\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{theorem}[Syntactic Type Soundness]
+\label{theorem:syntactic-soundness}
+No syntactically well-typed expression is stuck.
+
+Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\metavariable{\tau}\).
+Then it never occurs that \(\metavariable{e} \rightarrow_{\beta}^{*} \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}
 
+\begin{theorem}[Semantic Type Soundness]
+\label{theorem:semantic-soundness}
+No semantically well-typed expression is stuck.
 
+Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
+Then it never occurs that \(\llbracket D \rrbracket \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
+
+\begin{proof}
+Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
+By \ref{lemma:translation}, \(\emptyset \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
+and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
+\end{proof}
+\end{theorem}
+
+
+
+\newpage
 \section{Boehm-Berarducci Encoding}