diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 224999e236cf3c8ee5b098be6172263015c387a6..169dcfaeb3a06dfddd13b9babc6e58b397028b2d 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{\timeless{\prop} \and \prop \proves \later \propB}
+  \inferH{later-timeless-strip}{\timeless{\prop} \and \prop \proves \later \propB}
   {\later\prop \proves \later\propB}
 \end{mathpar}
 This rule looks different from the above ones, because we still do not have that