1 files changed, 19 insertions, 2 deletions
diff --git a/test/examples/datatype.tex b/test/examples/datatype.tex
index 3ea9161..09d014d 100644
--- a/test/examples/datatype.tex
+++ b/test/examples/datatype.tex
@@ -3,26 +3,43 @@
     Define $\propform$ inductively as follows.
     \begin{enumerate}
         \item $\propbot \in \propform$.
-        \item $\propvar{n} \in \propform$ for $n \in \{\emptyset\}$.
+        \item $\propvar{n} \in \propform$ for
+            $n \in \{\emptyset\}$.
         \item $(p \propto q) \in \propform$ for $p \in \propform$ and $q \in \propform$.
     \end{enumerate}
 \end{datatype}
 \begin{proposition}\label{propform_bot_test}
     $\propbot \in \propform$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{propform_propbot_intro}.
+\end{proof}
 
 \begin{proposition}\label{propform_var_test}
-    If $\emptyset \in \{\emptyset\}$, then $\propvar{\emptyset} \in \propform$.
+    If $\emptyset \in \{\emptyset\}$, then
+        $\propvar{\emptyset} \in \propform$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{propform_propvar_intro}.
+\end{proof}
 
 \begin{proposition}\label{propform_imp_test}
     $(\propbot \propto \propbot) \in \propform$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{propform_propbot_intro,propform_propto_intro}.
+\end{proof}
 
 \begin{proposition}\label{propform_distinct_test}
     $\propbot \neq (\propbot \propto \propbot)$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{propform_propbot_propto_distinct}.
+\end{proof}
 
 \begin{proposition}\label{propform_injective_test}
     If $\propvar{x} = \propvar{y}$, then $x = y$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{propform_propvar_injective}.
+\end{proof}