diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 2d259b3d372661d19dd79c5eab87ba6a741f0a3b..cdf29ac097628a993f8cc25ae2e07b0eb7361d15 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -64,7 +64,7 @@ In other words, when working below the except-0 modality, we can \emph{strip
   away} the later from timeless propositions. In fact, we can strip away later
 from timeless propositions even when working under the later modality:
 \begin{mathpar}
-  \infer{\prop \proves \later \propB}
+  \infer{\timeless{\prop} \and \prop \proves \later \propB}
   {\later\prop \proves \later\propB}
 \end{mathpar}