diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 169dcfaeb3a06dfddd13b9babc6e58b397028b2d..953a2fea746626d08472598cf0768ab57cf05625 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -72,6 +72,13 @@ This rule looks different from the above ones, because we still do not have that
   \inferH{later-fake-rule}{\timeless{\prop}}
   {\later\prop \proves \prop}
 \end{mathpar}
+The proof of the former is $\later \prop \proves \diamond \prop =
+\later\FALSE \lor \prop$, and then by straightforward disjunction elimination:
+% Cut the second part if trivial.
+\begin{mathpar}
+  \infer{\later\FALSE \proves \later \propB \and \prop \proves \later \propB}
+  {\later\FALSE \lor \prop \proves \propB}
+\end{mathpar}
 
 
 The following rules can be derived about except-0: