diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 8d15141405245ee9c6501c9b2338aa4b3bf05b53..2d259b3d372661d19dd79c5eab87ba6a741f0a3b 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -60,7 +60,13 @@ It turns out that we can somewhat mitigate this trouble by working below the fol
 
 This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, for which we have
 \[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop  \]
-In other words, when working below the except-0 modality, we can \emph{strip away} the later from timeless propositions.
+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}
+  {\later\prop \proves \later\propB}
+\end{mathpar}
 
 The following rules can be derived about except-0:
 \begin{mathpar}