diff --git a/coq/equiv.v b/coq/equiv.v
index a63789e..703d68c 100644
--- a/coq/equiv.v
+++ b/coq/equiv.v
@@ -37,7 +37,7 @@ Include Terms.
 Module Equiv.
 
 
-(** Define all rewrite steps *)
+(** Define all rewrite steps $\label{coq:type-dist}$ *)
 
 Reserved Notation "S '-->distribute-ladder' T" (at level 40).
 Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
@@ -111,7 +111,7 @@ Proof.
 Qed.
 
 
-(** Define the equivalence relation as reflexive, transitive hull. *)
+(** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *)
 
 Reserved Notation " S '===' T " (at level 40).
 Inductive type_eq : type_term -> type_term -> Prop :=
@@ -163,7 +163,7 @@ Proof.
   apply IHtype_eq1.
 Qed.
 
-(** "flat" types do not contain ladders *)
+(** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
 Inductive type_is_flat : type_term -> Prop :=
   | FlatUnit : (type_is_flat type_unit)
   | FlatVar : forall x, (type_is_flat (type_var x))
diff --git a/coq/subst.v b/coq/subst.v
index 1f2b0c8..c338fd6 100644
--- a/coq/subst.v
+++ b/coq/subst.v
@@ -4,8 +4,7 @@ Require Import terms.
 Include Terms.
 
 Module Subst.
-
-(* scoped variable substitution in type terms *)
+(* scoped variable substitution in type terms $\label{coq:subst-type}$ *)
 Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
   match t0 with
   | type_var name => if (eqb v name) then n else t0
diff --git a/paper/appendix.tex b/paper/appendix.tex
new file mode 100644
index 0000000..9826823
--- /dev/null
+++ b/paper/appendix.tex
@@ -0,0 +1,30 @@
+
+\onecolumn
+\appendix
+
+
+\section{Coq Listings}
+This document lists the Coq-Sourcecode from commit
+\input{|"git log -n 1 --oneline | cut -d' ' -f1"}.
+
+
+\subsection{terms.v}
+\label{coq:terms}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/terms.v}
+
+\subsection{subst.v}
+\label{coq:subst}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/subst.v}
+
+\subsection{equiv.v}
+\label{coq:equiv}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/equiv.v}
+
+\subsection{typing.v}
+\label{coq:typing}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/typing.v}
+
+\subsection{smallstep.v}
+\label{coq:smallstep}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/smallstep.v}
+
diff --git a/paper/main.tex b/paper/main.tex
index fa7c4cb..b77eeb7 100644
--- a/paper/main.tex
+++ b/paper/main.tex
@@ -4,7 +4,23 @@
 \usepackage{formal-grammar}
 \usepackage[dvipsnames]{xcolor}
 \usepackage{mathpartir}
+\usepackage{hyperref}
+\usepackage{url}
 
+\usepackage{minted}
+\usemintedstyle{tango}
+
+\DeclareUnicodeCharacter{2200}{$\forall$}
+\DeclareUnicodeCharacter{03C3}{$\sigma$}
+\DeclareUnicodeCharacter{03C4}{$\tau$}
+\DeclareUnicodeCharacter{03BB}{$\lambda$}
+\DeclareUnicodeCharacter{21A6}{$\mapsto$}
+\DeclareUnicodeCharacter{039B}{$\Lambda$}
+\DeclareUnicodeCharacter{03B1}{$\alpha$}
+\DeclareUnicodeCharacter{03B2}{$\beta$}
+\DeclareUnicodeCharacter{03B3}{$\gamma$}
+\DeclareUnicodeCharacter{03B4}{$\delta$}
+\DeclareUnicodeCharacter{0393}{$\Gamma$}
 
 \newcommand{\metavariable}[1]{\textcolor{teal}{#1}}
 \newcommand{\typeterminal}[1]{\textcolor{brown}{#1}}
@@ -296,10 +312,16 @@ in an expression \(
 
 \begin{definition}[Distributivity]
 \todo{}
+
+
+See \hyperref[coq:type-dist]{equiv.v:\ref{coq:type-dist}}.
 \end{definition}
 
 \begin{definition}[Equivalence Relation]
 \todo{}
+
+
+See \hyperref[coq:type-equiv]{equiv.v:\ref{coq:type-equiv}}.
 \end{definition}
 
 \subsubsection{Normal Forms}
@@ -717,5 +739,7 @@ pairs
 \subsection{Algebraic Datatypes}
 \todo{}
 
+\input{appendix}
+
 \end{document}