Add missing precondition

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}