diff git a/docs/ghoststate.tex b/docs/ghoststate.tex
index 953a2fea746626d08472598cf0768ab57cf05625..b8d55d0fd6249636244263d094b789a78286630c 100644
 a/docs/ghoststate.tex
+++ b/docs/ghoststate.tex
@@ 57,31 +57,7 @@ Persistence is preserved by conjunction, disjunction, separating conjunction as
One of the troubles of working in a stepindexed logic is the ``later'' modality $\later$.
It turns out that we can somewhat mitigate this trouble by working below the following \emph{except0} modality:
\[ \diamond \prop \eqdef \later\FALSE \lor \prop \]

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 except0 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}
 \inferH{latertimelessstrip}{\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
\begin{mathpar}
 \inferH{laterfakerule}{\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 except0:
+Except0 satisfies the usual laws of a ``monadic'' modality (similar to, \eg the update modalities):
\begin{mathpar}
\inferH{ex0mono}
{\prop \proves \propB}
@@ 106,6 +82,28 @@ The following rules can be derived about except0:
\diamond\later\prop &\proves& \later{\prop}
\end{array}
\end{mathpar}
+In particular, from \ruleref{ex0mono} and \ruleref{ex0idem} we can derive a ``bind''like elimination rule:
+\begin{mathpar}
+ \inferH{ex0elim}
+ {\prop \proves \diamond\propB}
+ {\diamond\prop \proves \diamond\propB}
+\end{mathpar}
+
+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 except0 modality, we can \emph{strip
+ away} the later from timeless propositions (using \ruleref{ex0elim}):
+\begin{mathpar}
+ \inferH{ex0timelessstrip}{\timeless{\prop} \and \prop \proves \diamond\propB}
+ {\later\prop \proves \diamond\propB}
+\end{mathpar}
+
+ In fact, it turns out that we can strip away later from timeless propositions even when working under the later modality:
+\begin{mathpar}
+ \inferH{latertimelessstrip}{\timeless{\prop} \and \prop \proves \later \propB}
+ {\later\prop \proves \later\propB}
+\end{mathpar}
+This follows from $\later \prop \proves \later\FALSE \lor \prop$, and then by straightforward disjunction elimination.
The following rules identify the class of timeless propositions:
\begin{mathparpagebreakable}