diff --git a/docs/constructions.tex b/docs/constructions.tex
index 0840acd32222463e44723b549f941a7245a83ee8..26cb9746e72aa0c08fdb461c32c3dde0131d0819 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -163,8 +163,6 @@ The step-indexed equivalence is inductively defined as follows:
 \begin{mathpar}
   \infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)}
 
-  \axiom{\munit \nequiv{n} \munit}
-
   \axiom{\bot \nequiv{n} \bot}
 \end{mathpar}
 $\exm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.