8 files changed, 53 insertions, 3 deletions
diff --git a/test/examples/coord.tex b/test/examples/coord.tex
index 9987506..32d3fa1 100644
--- a/test/examples/coord.tex
+++ b/test/examples/coord.tex
@@ -30,11 +30,17 @@
 \begin{proposition}\label{noun_verb}
     $x = y$ iff $x$ is a bar equal to $y$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{bar}.
+\end{proof}
 
 
 \begin{proposition}\label{adjs}
     $x$ is foo and baz.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{foo,baz}.
+\end{proof}
 
 \begin{proposition}\label{are_nouns}
     Let $x, y$ be foo bars.
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}
diff --git a/test/examples/finite-set-terms.tex b/test/examples/finite-set-terms.tex
index 76cc4d9..4aa7ba6 100644
--- a/test/examples/finite-set-terms.tex
+++ b/test/examples/finite-set-terms.tex
@@ -1,3 +1,7 @@
+\begin{signature}\label{example_cons}
+    $\cons{y}{X}$ is a set.
+\end{signature}
+
 \begin{axiom}\label{cons}
     $x\in \cons{y}{X}$ iff $x = y$ or $x\in X$.
 \end{axiom}
diff --git a/test/examples/proofdefinefunction.tex b/test/examples/proofdefinefunction.tex
index ac17d0b..0367a0d 100644
--- a/test/examples/proofdefinefunction.tex
+++ b/test/examples/proofdefinefunction.tex
@@ -1,3 +1,7 @@
+\begin{signature}\label{example_pair}
+    $(x,y)$ is a set.
+\end{signature}
+
 % The builtin "-(-)" notation desugars to "\apply{-}{-}".
 % This is just a dummy definition.
 \begin{definition}\label{apply}
diff --git a/test/examples/relation-notation.tex b/test/examples/relation-notation.tex
index 7cc94fc..0eff5d0 100644
--- a/test/examples/relation-notation.tex
+++ b/test/examples/relation-notation.tex
@@ -1,3 +1,7 @@
+\begin{signature}\label{example_pair}
+    $(x,y)$ is a set.
+\end{signature}
+
 \begin{proposition}\label{mathrel_notation_test}
     If $x\mathrel{R} y$, then $x\mathrel{R} y$.
 \end{proposition}
diff --git a/test/examples/replace.tex b/test/examples/replace.tex
index 66fae16..8737af3 100644
--- a/test/examples/replace.tex
+++ b/test/examples/replace.tex
@@ -1,3 +1,11 @@
+\begin{signature}\label{example_cons}
+    $\cons{y}{X}$ is a set.
+\end{signature}
+
+\begin{signature}\label{example_pair}
+    $(x,y)$ is a set.
+\end{signature}
+
 \begin{axiom}\label{cons}
     $x\in \cons{y}{X}$ iff $x = y$ or $x\in X$.
 \end{axiom}
@@ -25,3 +33,6 @@
 \begin{proposition}\label{times_replacement_test}
     $A\times B = \{ (a,b) \mid a\in A, b\in B\}$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{times}.
+\end{proof}
diff --git a/test/examples/russell.tex b/test/examples/russell.tex
index 4c2a8f2..dacd723 100644
--- a/test/examples/russell.tex
+++ b/test/examples/russell.tex
@@ -11,6 +11,6 @@
     Suppose not.
     Take a universal set $V$.
     Let $R = \{ x\in V \mid x\not\in x \}$.
-    Then $R\in R$ iff $R\not\in R$.
+    $R\in V$ by \cref{universal_set}.
     Contradiction.
 \end{proof}
diff --git a/test/examples/union.tex b/test/examples/union.tex
index b5c5783..cae5935 100644
--- a/test/examples/union.tex
+++ b/test/examples/union.tex
@@ -1,3 +1,7 @@
+\begin{signature}\label{example_union}
+    $A\union B$ is a set.
+\end{signature}
+
 \begin{axiom}[Extensionality]\label{ext}
     Suppose for all $a$ we have $a\in A$ iff $a\in B$.
     Then $A = B$.