diff --git a/thesis/main.tex b/thesis/main.tex
index aad9c6c..a3646c3 100644
--- a/thesis/main.tex
+++ b/thesis/main.tex
@@ -1,4 +1,4 @@
-\documentclass[a4paper,11pt,numbers=noenddot]{scrbook}
+\documentclass[a4paper,11pt,numbers=noenddot, draft]{scrbook}
 
 \usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry}
 \usepackage[ngerman, main=british]{babel}
@@ -104,7 +104,8 @@
 \makeatother
 
 
-\usepackage{noto-mono}
+% \usepackage{noto-mono}
+% TODO Need different mono font, noto-mono has weird font sizing...
 \usepackage{unicode-math}
 % \setmainfont{STIX-Regular}
 % \setmathfont{STIX Two Math Regular}
diff --git a/thesis/src/05_setoids.tex b/thesis/src/05_setoids.tex
index 4587af8..467e126 100644
--- a/thesis/src/05_setoids.tex
+++ b/thesis/src/05_setoids.tex
@@ -159,23 +159,19 @@ Now, we call two computations \(p\) and \(q\) \emph{weakly bisimilar} or \(p \ap
 \begin{proof}
   The monad unit is the constructor \texttt{now} and the multiplication can be defined as follows:
 
-  \begin{minted}{agda}
-    μ : Delay (Delay X) → Delay X
-    μ' : Delay' (Delay X) → Delay' X
-    μ (now x) = x
-    μ (later x) = later (μ' x)
-    force (μ' x) = μ (force x)
-  \end{minted}
+  \[\mu\;x = \begin{cases}
+      z             & \text{if } x = now\;z   \\
+      later(\mu\;z) & \text{if } x = later\;z
+    \end{cases}\]
 
   The monad laws have already been proven in~\cite{quotienting} and in our own formalization, so we will not reiterate the proofs here.
 \end{proof}
 
-\begin{theorem}
-  Every \((Delay\;A , \approx)\) can be equipped with a free Elgot algebra structure.
-\end{theorem}
+\begin{lemma}\label{lem:Delgot}
+  Every \((Delay\;A , \approx)\) can be equipped with an Elgot algebra structure.
+\end{lemma}
 \begin{proof}
-  We need to show that for every setoid \((A, =^A)\) the resulting setoid \((Delay\;A, \approx)\) can be extended to a free Elgot algebra.
-  % Stability follows automatically by \autoref{thm:stability} and the fact that \(\setoids\) is Cartesian closed, so it suffices to define a free Elgot Algebra on \((Delay\;A, \approx)\).
+  We need to show that for every setoid \((A, =^A)\) the resulting setoid \((Delay\;A, \approx)\) can be extended to an Elgot algebra.
 
   Let \((X , \overset{X}{=}) \in \obj{\setoids}\) and \(f : X \rightarrow Delay\; A + X\) be a setoid morphism, we define \(f^\sharp : X \rightarrow Delay\;A\) point wise:
   \[
@@ -260,8 +256,16 @@ Now, we call two computations \(p\) and \(q\) \emph{weakly bisimilar} or \(p \ap
             \end{alignat*}
           \end{mycase}
   \end{itemize}
-  This concludes the proof that every \((Delay\;A,\approx)\) can be extended to an Elgot algebra, let us now show that these Elgot algebras are free.
+  This concludes the proof that every \((Delay\;A,\approx)\) can be extended to an Elgot algebra.
+\end{proof}
 
+\todo[inline]{Discretization corollary here}
+
+\begin{theorem}\label{thm:Dfreeelgot}
+  Every \((Delay\;A , \approx)\) can be equipped with a free Elgot algebra structure.
+\end{theorem}
+\begin{proof}
+  We build on \autoref{lem:Delgot}, it thus suffices to show that the induced Elgot algebras are free.
   Given an Elgot algebra \((B , \overset{B}{=}, {(-)}^{\sharp_b})\) and a setoid morphism \(f : A \rightarrow B\). We need to define an Elgot algebra morphism \(\free{f} : Delay\;A \rightarrow B\). Consider \(g : Delay\;A \rightarrow B + Delay\;A\) defined by
   \[g\;x =
     \begin{cases}