Sketch proof

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: