diff --git a/docs/constructions.tex b/docs/constructions.tex
index 26cb9746e72aa0c08fdb461c32c3dde0131d0819..40571188f68a0ca7b4ec90de8acce72c8bd96b63 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -159,6 +159,8 @@ All cases of composition go to $\bot$.
   \mcore{\exinj(x)} \eqdef{}& \mnocore &
   \mcore{\bot} \eqdef{}& \bot
 \end{align*}
+Remember that $\mnocore$ is the ``dummy'' element in $\maybe\monoid$ indicating (in this case) that $\exinj(x)$ has no core.
+
 The step-indexed equivalence is inductively defined as follows:
 \begin{mathpar}
   \infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)}