diff --git a/blueprint/src/chapter/counterexamples.tex b/blueprint/src/chapter/counterexamples.tex
index b530037b..f44659df 100644
--- a/blueprint/src/chapter/counterexamples.tex
+++ b/blueprint/src/chapter/counterexamples.tex
@@ -1,18 +1,18 @@
 \chapter{Counterexamples}
 
-\begin{theorem}[46 does not imply 3]\label{46_not_imply_3}\lean{Equation46_not_implies_Equation3}\leanok\uses{eq46,eq3} Definition \ref{eq46} does not imply Definition \ref{eq3}.
+\begin{theorem}[46 does not imply 4]\label{46_not_imply_4}\lean{Equation46_not_implies_Equation4}\leanok\uses{eq46,eq4} Definition \ref{eq46} does not imply Definition \ref{eq4}.
 \end{theorem}
 
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y := 0$.
 \end{proof}
 
-\begin{theorem}[3 does not imply 4582]\label{3_not_imply_4582}\lean{Equation3_not_implies_Equation4582}\leanok\uses{eq3,eq4582} Definition \ref{eq3} does not imply Definition \ref{eq4582}.
+\begin{theorem}[4 does not imply 4582]\label{4_not_imply_4582}\lean{Equation4_not_implies_Equation4582}\leanok\uses{eq4,eq4582} Definition \ref{eq4} does not imply Definition \ref{eq4582}.
 \end{theorem}
 
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y := x$.
 \end{proof}
 
-\begin{theorem}[3 does not imply 43]\label{3_not_imply_43}\lean{Equation3_not_implies_Equation43}\leanok\uses{eq3,eq43} Definition \ref{eq3} does not imply Definition \ref{eq43}.
+\begin{theorem}[4 does not imply 43]\label{4_not_imply_43}\lean{Equation4_not_implies_Equation43}\leanok\uses{eq4,eq43} Definition \ref{eq4} does not imply Definition \ref{eq43}.
 \end{theorem}
 
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y := x$.
diff --git a/blueprint/src/chapter/implications.tex b/blueprint/src/chapter/implications.tex
index 959d6087..2bd5f68f 100644
--- a/blueprint/src/chapter/implications.tex
+++ b/blueprint/src/chapter/implications.tex
@@ -2,7 +2,7 @@ \chapter{Implications}
 
 To reduce clutter, trivial or very easy implications will not be displayed here.
 
-\begin{theorem}[387 implies 43]\label{387_implies_43}\uses{eq387,eq43}\lean{Equation4_implies_Equation43}\leanok  Definition \ref{eq387} implies Definition \ref{eq43}.
+\begin{theorem}[387 implies 43]\label{387_implies_43}\uses{eq387,eq43}\lean{Equation387_implies_Equation43}\leanok  Definition \ref{eq387} implies Definition \ref{eq43}.
 \end{theorem}
 
 \begin{proof}\leanok (From \href{https://mathoverflow.net/a/450905/766}{MathOverflow}).
diff --git a/blueprint/src/print.pdf b/blueprint/src/print.pdf
index 2528f0ac..a96eb15d 100644
Binary files a/blueprint/src/print.pdf and b/blueprint/src/print.pdf differ