diff --git a/algebra/upred.v b/algebra/upred.v
index 55bb3023d79a52a46a7b472e5a63f68ab4c2d356..1e8ee934b5ca9240bd86ba74c1a18e5710943148 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -917,8 +917,6 @@ Proof.
   unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
   apply HP, IH, uPred_weaken with (S n) x; eauto using cmra_validN_S.
 Qed.
-Lemma later_True' : True âŠ‘ (â–· True : uPred M).
-Proof. unseal; by split=> -[|n] x. Qed.
 Lemma later_and P Q : (â–· (P âˆ§ Q))%I â‰¡ (â–· P âˆ§ â–· Q)%I.
 Proof. unseal; split=> -[|n] x; by split. Qed.
 Lemma later_or P Q : (â–· (P âˆ¨ Q))%I â‰¡ (â–· P âˆ¨ â–· Q)%I.
@@ -927,9 +925,9 @@ Lemma later_forall {A} (Î¦ : A â†’ uPred M) : (â–· âˆ€ a, Î¦ a)%I â‰¡ (âˆ€ a, 
 Proof. unseal; by split=> -[|n] x. Qed.
 Lemma later_exist_1 {A} (Î¦ : A â†’ uPred M) : (âˆƒ a, â–· Î¦ a) âŠ‘ (â–· âˆƒ a, Î¦ a).
 Proof. unseal; by split=> -[|[|n]] x. Qed.
-Lemma later_exist `{Inhabited A} (Î¦ : A â†’ uPred M) :
-  (â–· âˆƒ a, Î¦ a)%I â‰¡ (âˆƒ a, â–· Î¦ a)%I.
-Proof. unseal; split=> -[|[|n]] x; split; done || by exists inhabitant. Qed.
+Lemma later_exist' `{Inhabited A} (Î¦ : A â†’ uPred M) :
+  (â–· âˆƒ a, Î¦ a)%I âŠ‘ (âˆƒ a, â–· Î¦ a)%I.
+Proof. unseal; split=> -[|[|n]] x; done || by exists inhabitant. Qed.
 Lemma later_sep P Q : (â–· (P â˜… Q))%I â‰¡ (â–· P â˜… â–· Q)%I.
 Proof.
   unseal; split=> n x ?; split.
@@ -949,12 +947,15 @@ Global Instance later_flip_mono' :
   Proper (flip (âŠ‘) ==> flip (âŠ‘)) (@uPred_later M).
 Proof. intros P Q; apply later_mono. Qed.
 Lemma later_True : (â–· True : uPred M)%I â‰¡ True%I.
-Proof. apply (anti_symm (âŠ‘)); auto using later_True'. Qed.
+Proof. apply (anti_symm (âŠ‘)); auto using later_intro. Qed.
 Lemma later_impl P Q : â–· (P â†’ Q) âŠ‘ (â–· P â†’ â–· Q).
 Proof.
   apply impl_intro_l; rewrite -later_and.
   apply later_mono, impl_elim with P; auto.
 Qed.
+Lemma later_exist `{Inhabited A} (Î¦ : A â†’ uPred M) :
+  (â–· âˆƒ a, Î¦ a)%I â‰¡ (âˆƒ a, â–· Î¦ a)%I.
+Proof. apply: anti_symm; eauto using later_exist', later_exist_1. Qed.
 Lemma later_wand P Q : â–· (P -â˜… Q) âŠ‘ (â–· P -â˜… â–· Q).
 Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
 Lemma later_iff P Q : (â–· (P â†” Q)) âŠ‘ (â–· P â†” â–· Q).
diff --git a/docs/logic.tex b/docs/logic.tex
index bad60509ed4ffd285d642d515737b91d38882be3..6e1ead9f3b55d074f70aab3c1dedba9fc8b612bf 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -120,6 +120,8 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
 \end{align*}
 Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable $\var$ can only appear under the later $\later$ modality.
 
+Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
+
 \paragraph{Metavariable conventions.}
 We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:
 \[
@@ -292,7 +294,6 @@ Axioms $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \R
 \judgment{}{\vctx \mid \pfctx \proves \prop}
 \paragraph{Laws of intuitionistic higher-order logic.}
 This is entirely standard.
-
 \begin{mathparpagebreakable}
 \infer[Asm]
   {\prop \in \pfctx}
@@ -384,18 +385,17 @@ This is entirely standard.
   (\prop * \propB) * \propC &\Lra& \prop * (\propB * \propC)
 \end{array}
 \and
-\infer
+\infer[$*$-mono]
   {\prop_1 \proves \propB_1 \and
    \prop_2 \proves \propB_2}
   {\prop_1 * \prop_2 \proves \propB_1 * \propB_2}
 \and
-\inferB
+\inferB[$\wand$I-E]
   {\prop * \propB \proves \propC}
   {\prop \proves \propB \wand \propC}
 \end{mathpar}
 
 \paragraph{Laws for ghosts and physical resources.}
-
 \begin{mathpar}
 \begin{array}{rMcMl}
 \ownGGhost{\melt} * \ownGGhost{\meltB} &\Lra&  \ownGGhost{\melt \mtimes \meltB} \\
@@ -409,60 +409,59 @@ This is entirely standard.
 \end{mathpar}
 
 \paragraph{Laws for the later modality.}
-~\\\ralf{Go on checking below.}
-
-
 \begin{mathpar}
-\inferH{Mono}
+\infer[$\later$-mono]
   {\pfctx \proves \prop}
   {\pfctx \proves \later{\prop}}
 \and
-\inferhref{L{\"o}b}{Loeb}
-  {\pfctx, \later{\prop} \proves \prop}
-  {\pfctx \proves \prop}
+\infer[L{\"o}b]
+  {}
+  {(\later\prop\Ra\prop) \proves \prop}
 \and
-\begin{array}[b]{rMcMl}
-  \later{\always{\prop}} &\Lra& \always{\later{\prop}} \\
+\infer[$\later$-$\exists$]
+  {\text{$\type$ is inhabited}}
+  {\later{\Exists x:\type.\prop} \proves \Exists x:\type. \later\prop}
+\\\\
+\begin{array}[c]{rMcMl}
   \later{(\prop \wedge \propB)} &\Lra& \later{\prop} \wedge \later{\propB}  \\
   \later{(\prop \vee \propB)} &\Lra& \later{\prop} \vee \later{\propB} \\
 \end{array}
 \and
-\begin{array}[b]{rMcMl}
+\begin{array}[c]{rMcMl}
   \later{\All x.\prop} &\Lra& \All x. \later\prop \\
-  \later{\Exists x.\prop} &\Lra& \Exists x. \later\prop \\
+  \Exists x. \later\prop &\Ra& \later{\Exists x.\prop}  \\
   \later{(\prop * \propB)} &\Lra& \later\prop * \later\propB
 \end{array}
 \end{mathpar}
 
 \paragraph{Laws for the always modality.}
-
 \begin{mathpar}
-\axiomH{Necessity}
-  {\always{\prop} \Ra \prop}
-\and
-\inferhref{$\always$I}{AlwaysIntro}
+\infer[$\always$I]
   {\always{\pfctx} \proves \prop}
   {\always{\pfctx} \proves \always{\prop}}
 \and
-\begin{array}[b]{rMcMl}
-  \always(\term =_\type \termB) &\Lra& \term=_\type \termB \\
-  \always{\prop} * \propB &\Lra& \always{\prop} \land \propB \\
-  \always{(\prop \Ra \propB)} &\Ra& \always{\prop} \Ra \always{\propB} \\
+\infer[$\always$E]{}
+  {\always{\prop} \Ra \prop}
+\and
+\begin{array}[c]{rMcMl}
+  \always{(\prop * \propB)} &\Ra& \always{(\prop \land \propB)} \\
+  \always{\prop} * \propB &\Ra& \always{\prop} \land \propB \\
+  \always{\later\prop} &\Lra& \later\always{\prop} \\
 \end{array}
 \and
-\begin{array}[b]{rMcMl}
+\begin{array}[c]{rMcMl}
   \always{(\prop \land \propB)} &\Lra& \always{\prop} \land \always{\propB} \\
   \always{(\prop \lor \propB)} &\Lra& \always{\prop} \lor \always{\propB} \\
   \always{\All x. \prop} &\Lra& \All x. \always{\prop} \\
   \always{\Exists x. \prop} &\Lra& \Exists x. \always{\prop} \\
 \end{array}
 \end{mathpar}
-Note that $\always$ binds more tightly than $*$, $\land$, $\lor$, and $\Ra$.
 
 \paragraph{Laws of primitive view shifts.}
+~\\\ralf{Add these.}
 
 \paragraph{Laws of weakest preconditions.}
-
+~\\\ralf{Add these.}
 
 %%% Local Variables:
 %%% mode: latex