diff git a/CHANGELOG.md b/CHANGELOG.md
index 9e762c041ffcc1693bc4f281489cf96516ecc53a..224ed688a59c021d1729802d5b8f8e15a18538dd 100644
 a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ 24,10 +24,10 @@ Changes in and extensions of the theory:
trace has a matching list of events. Change WP so that it is told the entire
future trace of observations from the beginning. Use this in heap_lang to
implement prophecy variables.
* [#] The Löb rule is now a derived rule; it follows from laterintro, later
+* The Löb rule is now a derived rule; it follows from laterintro, later
being contractive and the fact that we can take fixpoints of contractive
functions.
* [#] Add atomic updates and logically atomic triples, including tactic support.
+* Add atomic updates and logically atomic triples, including tactic support.
See `heap_lang/lib/increment.v` for an example.
* [#] heap_lang now uses righttoleft evaluation order. This makes it
significantly easier to write specifications of curried functions.
diff git a/docs/baselogic.tex b/docs/baselogic.tex
index 450b6a6adc6c83a3e6ebbf606b6817c588daa7b2..344ed6d0a9a59a2ba099e3a191f2fd6b01e37807 100644
 a/docs/baselogic.tex
+++ b/docs/baselogic.tex
@@ 380,9 +380,9 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\textlo
{\prop \proves \propB}
{\later\prop \proves \later{\propB}}
\and
\inferhref{L{\"o}b}{Loeb}
+\infer[$\later$I]
{}
 {(\later\prop\Ra\prop) \proves \prop}
+ {\prop \proves \later\prop}
\and
\begin{array}[c]{rMcMl}
\All x. \later\prop &\proves& \later{\All x.\prop} \\
diff git a/docs/ghoststate.tex b/docs/ghoststate.tex
index c774af1077f8aaf39a7cfc3ccbc74535f21e2e44..7dbf916a9f9d0f1e8b8b9558acedcc1edb5e8d89 100644
 a/docs/ghoststate.tex
+++ b/docs/ghoststate.tex
@@ 6,6 +6,10 @@ These are not ``extensions'' in the sense that they change the proof power of th
\subsection{Derived Rules about Base Connectives}
We collect here some important and frequently used derived proof rules.
\begin{mathparpagebreakable}
+ \inferhref{L{\"o}b}{Loeb}
+ {}
+ {(\later\prop\Ra\prop) \proves \prop}
+
\infer{}
{\prop \Ra \propB \proves \prop \wand \propB}
@@ 33,14 +37,14 @@ We collect here some important and frequently used derived proof rules.
\infer{}
{\later(\prop \wand \propB) \proves \later\prop \wand \later\propB}
 \infer{}
 {\prop \proves \later\prop}

\infer{}
{\TRUE \proves \plainly\TRUE}
\end{mathparpagebreakable}
Noteworthy here is the fact that $\prop \proves \later\prop$ can be derived from Löb induction, and $\TRUE \proves \plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$.
+Noteworthy here is the fact that Löb induction can be derived from $\later$introduction and the fact that we can take fixedpoints of functions where the recursive occurrences are below $\later$.%
+\footnote{See \url{https://en.wikipedia.org/wiki/L\%C3\%B6b\%27s_theorem}.}
+Furthermore, $\TRUE \proves \plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$.
+To derive that existential quantifiers commute with separating conjunction requires an intermediate step using a magic wand: From $P * \exists x, Q \vdash \Exists x. P * Q$ we can deduce $\Exists x. Q \vdash P \wand \Exists x. P * Q$ and then proceed via $\exists$elimination.
\subsection{Persistent Propositions}
We call a proposition $\prop$ \emph{persistent} if $\prop \proves \always\prop$.