diff --git a/paper/appendix.tex b/paper/appendix.tex
index 9826823..aa2c75b 100644
--- a/paper/appendix.tex
+++ b/paper/appendix.tex
@@ -20,11 +20,23 @@ This document lists the Coq-Sourcecode from commit
 \label{coq:equiv}
 \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/equiv.v}
 
+\subsection{subtype.v}
+\label{coq:typing}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/subtype.v}
+
 \subsection{typing.v}
 \label{coq:typing}
 \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/typing.v}
 
+\subsection{morph.v}
+\label{coq:typing}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/morph.v}
+
 \subsection{smallstep.v}
 \label{coq:smallstep}
 \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/smallstep.v}
 
+\subsection{soundness.v}
+\label{coq:smallstep}
+\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/soundness.v}
+