diff --git a/blueprint/src/chapter/counterexamples.tex b/blueprint/src/chapter/counterexamples.tex
index 6ac6e36d..b530037b 100644
--- a/blueprint/src/chapter/counterexamples.tex
+++ b/blueprint/src/chapter/counterexamples.tex
@@ -66,3 +66,15 @@ \chapter{Counterexamples}
 
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y := x + y$.
 \end{proof}
+
+\begin{theorem}[Equation 387 does not imply Equation 42]\label{387_not_imply_42}\lean{Equation387_not_implies_Equation42}\leanok\uses{eq387,eq42} Definition \ref{eq387} does not imply Definition \ref{eq42}.
+\end{theorem}
+
+\begin{proof} ???
+\end{proof}
+
+\begin{theorem}[Equation 43 does not imply Equation 387]\label{43_not_imply_387}\lean{Equation43_not_implies_Equation387}\leanok\uses{eq43,eq387} Definition \ref{eq43} does not imply Definition \ref{eq387}.
+\end{theorem}
+
+\begin{proof} ???
+\end{proof}
diff --git a/blueprint/src/print.pdf b/blueprint/src/print.pdf
index c801ebaa..2528f0ac 100644
Binary files a/blueprint/src/print.pdf and b/blueprint/src/print.pdf differ
diff --git a/equational_theories/Basic.lean b/equational_theories/Basic.lean
index d2728607..219ef672 100644
--- a/equational_theories/Basic.lean
+++ b/equational_theories/Basic.lean
@@ -243,3 +243,9 @@ theorem Equation4512_not_implies_Equation42 : ∃ (G: Type) (_: Magma G), Equati
   replace h := h 0 0 1
   dsimp [hG] at h
   linarith
+
+theorem Equation387_not_implies_Equation42 : ∃ (G: Type) (_: Magma G), Equation387 G ∧ ¬ Equation42 G := by
+  sorry
+
+theorem Equation43_not_implies_Equation387 : ∃ (G: Type) (_: Magma G), Equation387 G ∧ ¬ Equation42 G := by
+  sorry