diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 6390b968d567d829b5dd92cd56164a2db2ba69f3..ed3f8e77278f50eeb59ae47e89cb0406065ad78a 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -14,7 +14,7 @@ To this end, we use tokens that manage which invariants are currently enabled.
 
 We assume to have the following four CMRAs available:
 \begin{align*}
-  \textmon{State} \eqdef{}& \authm(\exm(\State)) \\
+  \textmon{State} \eqdef{}& \authm(\maybe{\exm(\State)}) \\
   \textmon{Inv} \eqdef{}& \authm(\nat \fpfn \agm(\latert \iPreProp)) \\
   \textmon{En} \eqdef{}& \pset{\nat} \\
   \textmon{Dis} \eqdef{}& \finpset{\nat}