diff --git a/CHANGELOG.md b/CHANGELOG.md
index a1b9a8f564b1985c058ac61a135ddd74a08f2afe..98c97a38422f23fa6b8b1f4f4073d5a6044b1b72 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,9 +15,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * With invariants and the physical state being handled in the logic, there
   is no longer any reason to demand the CMRA unit to be discrete.
 * The language can now fork off multiple threads at once.
-* [#] Local Updates (for the authoritative monoid) are now a 4-way relation
-  with syntax-directed lemmas proving them.  [program_logic/auth] is gone,
-  it doesn't actually simplify anything any more.
+* Local Updates (for the authoritative monoid) are now a 4-way relation
+  with syntax-directed lemmas proving them.
 
 ## Iris 2.0
 
diff --git a/algebra/upred.v b/algebra/upred.v
index d3ddbbcd8b39c22bb66c40ecfc6117a712fbfe68..8d8baee242e1001d4286221430df5c3402e1df6f 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -821,26 +821,25 @@ Proof.
   split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x;
     eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
 Qed.
-Global Instance True_sep : LeftId (⊣⊢) True%I (@uPred_sep M).
+Lemma True_sep_1 P : P ⊢ True ★ P.
 Proof.
-  intros P; unseal; split=> n x Hvalid; split.
-  - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_mono, cmra_includedN_r.
-  - by intros ?; exists (core x), x; rewrite cmra_core_l.
+  unseal; split; intros n x ??. exists (core x), x. by rewrite cmra_core_l.
 Qed.
-Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M).
+Lemma True_sep_2 P : True ★ P ⊢ P.
 Proof.
-  by intros P Q; unseal; split=> n x ?; split;
-    intros (x1&x2&?&?&?); exists x2, x1; rewrite (comm op).
+  unseal; split; intros n x ? (x1&x2&?&_&?); cofe_subst;
+    eauto using uPred_mono, cmra_includedN_r.
 Qed.
-Global Instance sep_assoc : Assoc (⊣⊢) (@uPred_sep M).
+Lemma sep_comm' P Q : P ★ Q ⊢ Q ★ P.
+Proof.
+  unseal; split; intros n x ? (x1&x2&?&?&?); exists x2, x1; by rewrite (comm op).
+Qed.
+Lemma sep_assoc' P Q R : (P ★ Q) ★ R ⊢ P ★ (Q ★ R).
 Proof.
-  intros P Q R; unseal; split=> n x ?; split.
-  - intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 â‹… y1), y2; split_and?; auto.
-    + by rewrite -(assoc op) -Hy -Hx.
-    + by exists x1, y1.
-  - intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 â‹… x2); split_and?; auto.
-    + by rewrite (assoc op) -Hy -Hx.
-    + by exists y2, x2.
+  unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?).
+  exists y1, (y2 â‹… x2); split_and?; auto.
+  + by rewrite (assoc op) -Hy -Hx.
+  + by exists y2, x2.
 Qed.
 Lemma wand_intro_r P Q R : (P ★ Q ⊢ R) → P ⊢ Q -★ R.
 Proof.
@@ -872,6 +871,15 @@ Qed.
 Global Instance wand_mono' : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@uPred_wand M).
 Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
 
+Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M).
+Proof. intros P Q; apply (anti_symm _); auto using sep_comm'. Qed.
+Global Instance sep_assoc : Assoc (⊣⊢) (@uPred_sep M).
+Proof.
+  intros P Q R; apply (anti_symm _); auto using sep_assoc'.
+  by rewrite !(comm _ P) !(comm _ _ R) sep_assoc'.
+Qed.
+Global Instance True_sep : LeftId (⊣⊢) True%I (@uPred_sep M).
+Proof. intros P; apply (anti_symm _); auto using True_sep_1, True_sep_2. Qed.
 Global Instance sep_True : RightId (⊣⊢) True%I (@uPred_sep M).
 Proof. by intros P; rewrite comm left_id. Qed.
 Lemma sep_elim_l P Q : P ★ Q ⊢ P.
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index e2e95048417f1c33512b3e52b718cf895e2d8462..a0817ead9e0ec2faba0495828f0ddc5d37d1a343 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -289,8 +289,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 \begin{mathpar}
 \begin{array}{rMcMl}
   \TRUE * \prop &\provesIff& \prop \\
-  \prop * \propB &\provesIff& \propB * \prop \\
-  (\prop * \propB) * \propC &\provesIff& \prop * (\propB * \propC)
+  \prop * \propB &\proves& \propB * \prop \\
+  (\prop * \propB) * \propC &\proves& \prop * (\propB * \propC)
 \end{array}
 \and
 \infer[$*$-mono]
@@ -339,17 +339,17 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 \begin{array}[c]{rMcMl}
   \All x. \later\prop &\proves& \later{\All x.\prop} \\
   \later\Exists x. \prop &\proves& \later\FALSE \lor {\Exists x.\later\prop}  \\
-  \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop) \\
+  \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop)
 \end{array}
 \and
 \begin{array}[c]{rMcMl}
   \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\
-  \always{\later\prop} &\provesIff& \later\always{\prop} \\
+  \always{\later\prop} &\provesIff& \later\always{\prop}
 \end{array}
 \end{mathpar}
 
 
-\paragraph{Laws for ghosts and validity.}
+\paragraph{Laws for resources and validity.}
 \begin{mathpar}
 \begin{array}{rMcMl}
 \ownM{\melt} * \ownM{\meltB} &\provesIff&  \ownM{\melt \mtimes \meltB} \\
@@ -357,14 +357,14 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 \TRUE &\proves&  \ownM{\munit} \\
 \later\ownM\melt &\proves& \Exists\meltB. \ownM\meltB \land \later(\melt = \meltB)
 \end{array}
-\and
-\infer[valid-intro]
-{\melt \in \mval}
-{\TRUE \vdash \mval(\melt)}
-\and
-\infer[valid-elim]
-{\melt \notin \mval_0}
-{\mval(\melt) \proves \FALSE}
+% \and
+% \infer[valid-intro]
+% {\melt \in \mval}
+% {\TRUE \vdash \mval(\melt)}
+% \and
+% \infer[valid-elim]
+% {\melt \notin \mval_0}
+% {\mval(\melt) \proves \FALSE}
 \and
 \begin{array}{rMcMl}
 \ownM{\melt} &\proves& \mval(\melt) \\
@@ -376,24 +376,26 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 
 \paragraph{Laws for the resource update modality.}
 \begin{mathpar}
-\infer[upd-mono]
+\inferH{upd-mono}
 {\prop \proves \propB}
 {\upd\prop \proves \upd\propB}
 
-\infer[upd-intro]
+\inferH{upd-intro}
 {}{\prop \proves \upd \prop}
 
-\infer[upd-trans]
+\inferH{upd-trans}
 {}
 {\upd \upd \prop \proves \upd \prop}
 
-\infer[upd-frame]
+\inferH{upd-frame}
 {}{\propB * \upd\prop \proves \upd (\propB * \prop)}
 
 \inferH{upd-update}
 {\melt \mupd \meltsB}
 {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
 \end{mathpar}
+The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.
+\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
 
 \subsection{Consistency}
 
diff --git a/docs/constructions.tex b/docs/constructions.tex
index eceb03316643585a2ee0c4b72ebe51d8a1645982..e7607889b4b425cf59597252ded7b15296ab9112 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -1,4 +1,3 @@
-% !TEX root = ./appendix.tex
 \section{COFE constructions}
 
 \subsection{Next (type-level later)}
@@ -254,126 +253,41 @@ We obtain the following frame-preserving update:
 % \end{proof}
 
 
-% %\subsection{Disposable monoid}
-% %
-% %Given a monoid $M$, we construct a monoid where, having full ownership of an element $\melt$ of $M$, one can throw it away, transitioning to a dead element.
-% %Let \dispm{M} be the monoid with carrier $\mcarp{M} \uplus \{ \disposed \}$ and multiplication
-% %% The previous unit must remain the unit of the new monoid, as is is always duplicable and hence we could not transition to \disposed if it were not composable with \disposed
-% %\begin{align*}
-% %  \melt \mtimes \meltB &\eqdef \melt \mtimes_M \meltB & \IF \melt \sep[M] \meltB \\
-% %  \disposed \mtimes \disposed &\eqdef \disposed \\
-% %  \munit_M \mtimes \disposed &\eqdef \disposed \mtimes \munit_M \eqdef \disposed
-% %\end{align*}
-% %The unit is the same as in $M$.
-% %
-% %The frame-preserving updates are
-% %\begin{mathpar}
-% % \inferH{DispUpd}
-% %   {a \in \mcarp{M} \setminus \{\munit_M\} \and a \mupd_M B}
-% %   {a \mupd B}
-% % \and
-% % \inferH{Dispose}
-% %  {a \in \mcarp{M} \setminus \{\munit_M\} \and \All b \in \mcarp{M}. a \sep b \Ra b = \munit_M}
-% %  {a \mupd \disposed}
-% %\end{mathpar}
-% %
-% %\begin{proof}[Proof of \ruleref{DispUpd}]
-% %Assume a frame $f$. If $f = \disposed$, then $a = \munit_M$, which is a contradiction.
-% %Thus $f \in \mcarp{M}$ and we can use $a \mupd_M B$.
-% %\end{proof}
-% %
-% %\begin{proof}[Proof of \ruleref{Dispose}]
-% %The second premiss says that $a$ has no non-trivial frame in $M$. To show the update, assume a frame $f$ in $\dispm{M}$. Like above, we get $f \in \mcarp{M}$, and thus $f = \munit_M$. But $\disposed \sep \munit_M$ is trivial, so we are done.
-% %\end{proof}
-
-% \subsection{Authoritative monoid}\label{sec:auth}
-
-% Given a monoid $M$, we construct a monoid modeling someone owning an \emph{authoritative} element $x$ of $M$, and others potentially owning fragments $\melt \le_M x$ of $x$.
-% (If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
-% Let $\auth{M}$ be the monoid with carrier
-% \[
-% 	\setComp{ (x, \melt) }{ x \in \mcarp{\exm{\mcarp{M}}} \land \melt \in \mcarp{M} \land (x = \munit_{\exm{\mcarp{M}}} \lor \melt \leq_M x) }
-% \]
-% and multiplication
-% \[
-% (x, \melt) \mtimes (y, \meltB) \eqdef
-%      (x \mtimes y, \melt \mtimes \meltB) \quad \mbox{if } x \sep y \land \melt \sep \meltB \land (x \mtimes y = \munit_{\exm{\mcarp{M}}} \lor \melt \mtimes \meltB \leq_M x \mtimes y)
-% \]
-% Note that $(\munit_{\exm{\mcarp{M}}}, \munit_M)$ is the unit and asserts no ownership whatsoever, but $(\munit_{M}, \munit_M)$ asserts that the authoritative element is $\munit_M$.
-
-% Let $x, \melt \in \mcarp M$.
-% We write $\authfull x$ for full ownership $(x, \munit_M):\auth{M}$ and $\authfrag \melt$ for fragmental ownership $(\munit_{\exm{\mcarp{M}}}, \melt)$ and $\authfull x , \authfrag \melt$ for combined ownership $(x, \melt)$.
-% If $x$ or $a$ is $\mzero_{M}$, then the sugar denotes $\mzero_{\auth{M}}$.
-
-% \ralf{This needs syncing with the Coq development.}
-% The frame-preserving update involves a rather unwieldy side-condition:
-% \begin{mathpar}
-% 	\inferH{AuthUpd}{
-% 		\All\melt_\f\in\mcar{\monoid}. \melt\sep\meltB \land \melt\mtimes\melt_\f \le \meltB\mtimes\melt_\f \Ra \melt'\mtimes\melt_\f \le \melt'\mtimes\meltB \and
-% 		\melt' \sep \meltB
-% 	}{
-% 		\authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \melt' \mtimes \meltB, \authfrag \melt'
-% 	}
-% \end{mathpar}
-% We therefore derive two special cases.
-
-% \paragraph{Local frame-preserving updates.}
-
-% \newcommand\authupd{f}%
-% Following~\cite{scsl}, we say that $\authupd: \mcar{M} \ra \mcar{M}$ is \emph{local} if
-% \[
-% 	\All a, b \in \mcar{M}. a \sep b \land \authupd(a) \neq \mzero \Ra \authupd(a \mtimes b) = \authupd(a) \mtimes b
-% \]
-% Then,
-% \begin{mathpar}
-% 	\inferH{AuthUpdLocal}
-% 	{\text{$\authupd$ local} \and \authupd(\melt)\sep\meltB}
-% 	{\authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \authupd(\melt) \mtimes \meltB, \authfrag \authupd(\melt)}
-% \end{mathpar}
-
-% \paragraph{Frame-preserving updates on cancellative monoids.}
+\subsection{Authoritative}
+\label{sec:auth-cmra}
 
-% Frame-preserving updates are also possible if we assume $M$ cancellative:
-% \begin{mathpar}
-%  \inferH{AuthUpdCancel}
-%   {\text{$M$ cancellative} \and \melt'\sep\meltB}
-%   {\authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \melt' \mtimes \meltB, \authfrag \melt'}
-% \end{mathpar}
+Given a CMRA $M$, we construct $\authm(M)$ modeling someone owning an \emph{authoritative} element $\melt$ of $M$, and others potentially owning fragments $\meltB \mincl \melt$ of $\melt$.
+We assume that $M$ has a unit $\munit$, and hence its core is total.
+(If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
+\begin{align*}
+\authm(M) \eqdef{}& \maybe{\exm(M)} \times M \\
+\mval_n \eqdef{}& \setComp{ (x, \meltB) \in \authm(M) }{ \meltB \in \mval_n \land (x = \mnocore \lor \Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt) } \\
+  (x_1, \meltB_1) \mtimes (x_2, \meltB_2) \eqdef{}& (x_1 \mtimes x_2, \meltB_2 \mtimes \meltB_2) \\
+  \mcore{(x, \meltB)} \eqdef{}& (\mnocore, \mcore\meltB) \\
+  (x_1, \meltB_1) \nequiv{n} (x_2, \meltB_2) \eqdef{}& x_1 \nequiv{n} x_2 \land \meltB_1 \nequiv{n} \meltB_2
+\end{align*}
+Note that $(\mnocore, \munit)$ is the unit and asserts no ownership whatsoever, but $(\exinj(\munit), \munit)$ asserts that the authoritative element is $\munit$.
 
-% \subsection{Fractional heap monoid}
-% \label{sec:fheapm}
+Let $\melt, \meltB \in M$.
+We write $\authfull \melt$ for full ownership $(\exinj(\melt), \munit)$ and $\authfrag \meltB$ for fragmental ownership $(\mnocore, \meltB)$ and $\authfull \melt , \authfrag \meltB$ for combined ownership $(\exinj(\melt), \meltB)$.
 
-% By combining the fractional, finite partial function, and authoritative monoids, we construct two flavors of heaps with fractional permissions and mention their important frame-preserving updates.
-% Hereinafter, we assume the set $\textdom{Val}$ of values is countable.
+The frame-preserving update involves the notion of a \emph{local update}:
+\newcommand\lupd{\stackrel{\mathrm l}{\mupd}}
+\begin{defn}
+  It is possible to do a \emph{local update} from $\melt_1$ and $\meltB_1$ to $\melt_2$ and $\meltB_2$, written $(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)$, if
+  \[ \All n, \maybe{\melt_\f}. x_1 \in \mval_n \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra \melt_2 \in \mval_n \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
+\end{defn}
+In other words, the idea is that for every possible frame $\maybe{\melt_\f}$ completing $\meltB_1$ to $\melt_1$, the same frame also completes $\meltB_2$ to $\melt_2$.
 
-% Given a set $Y$, define $\FHeap(Y) \eqdef \textdom{Val} \fpfn \fracm(Y)$ representing a fractional heap with codomain $Y$.
-% From \S\S\ref{sec:fracm} and~\ref{sec:fpfunm} we obtain the following frame-preserving updates as well as the fact that $\FHeap(Y)$ is cancellative.
-% \begin{mathpar}
-% 	\axiomH{FHeapUpd}{h[x \mapsto (1, y)] \mupd h[x \mapsto (1, y')]} \and
-% 	\axiomH{FHeapAlloc}{h \mupd \{\, h[x \mapsto (1, y)] \mid x \in \textdom{Val} \,\}}
-% \end{mathpar}
-% We will write $qh$ with $h : \textsort{Val} \fpfn Y$ for the function in $\FHeap(Y)$ mapping every $x \in \dom(h)$ to $(q, h(x))$, and everything else to $\munit$.
-
-% Define $\AFHeap(Y) \eqdef \auth{\FHeap(Y)}$ representing an authoritative fractional heap with codomain $Y$.
-% We easily obtain the following frame-preserving updates.
-% \begin{mathpar}
-% 	\axiomH{AFHeapUpd}{
-% 		(\authfull h[x \mapsto (1, y)], \authfrag [x \mapsto (1, y)]) \mupd (\authfull h[x \mapsto (1, y')], \authfrag [x \mapsto (1, y')])
-% 	}
-% 	\and
-% 	\inferH{AFHeapAdd}{
-% 		x \notin \dom(h)
-% 	}{
-% 		\authfull h \mupd (\authfull h[x \mapsto (q, y)], \authfrag [x \mapsto (q, y)])
-% 	}
-% 	\and
-% 	\axiomH{AFHeapRemove}{
-% 		(\authfull h[x \mapsto (q, y)], \authfrag [x \mapsto (q, y)]) \mupd \authfull h
-% 	}
-% \end{mathpar}
+We then obtain
+\begin{mathpar}
+  \inferH{auth-update}
+  {(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)}
+  {\authfull \melt_1 , \authfrag \meltB_1 \mupd \authfull \melt_2 , \authfrag \meltB_2}
+\end{mathpar}
 
 \subsection{STS with tokens}
-\label{sec:stsmon}
+\label{sec:sts-cmra}
 
 Given a state-transition system~(STS, \ie a directed graph) $(\STSS, {\stsstep} \subseteq \STSS \times \STSS)$, a set of tokens $\STST$, and a labeling $\STSL: \STSS \ra \wp(\STST)$ of \emph{protocol-owned} tokens for each state, we construct an RA modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens.
 
diff --git a/docs/iris.sty b/docs/iris.sty
index c3bee3ef476d57c1fb1d3ff15e1de5d8ed3d7e1a..656e4586166dd9066790b404ae4fc321aba80fad 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -28,6 +28,8 @@
 %% MATH SYMBOLS & NOTATION & IDENTIFIERS
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\newcommand{\nat}{\mathbb{N}}
+
 \DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
 \newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
 \newcommand\pord{\sqsubseteq}
@@ -35,7 +37,7 @@
 \newcommand{\upclose}{\mathord{\uparrow}}
 \newcommand{\ALT}{\ |\ }
 
-\newcommand{\spac}{\:} % a space
+\newcommand{\spac}{\,} % a space
 
 \def\All #1.{\forall #1.\spac}%
 \def\Exists #1.{\exists #1.\spac}%
@@ -80,6 +82,12 @@
 
 \newcommand{\Func}{F} % functor
 
+\newcommand{\subst}[3]{{#1}[{#3} / {#2}]}
+
+\newcommand{\mapinsert}[3]{#3[#1:=#2]}
+
+\newcommand{\nil}{\epsilon}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -122,6 +130,10 @@
 \newcommand{\iPreProp}{\textdom{iPreProp}}
 \newcommand{\Wld}{\textdom{Wld}}
 \newcommand{\Res}{\textdom{Res}}
+\newcommand{\State}{\textdom{State}}
+\newcommand{\Val}{\textdom{Val}}
+\newcommand{\Loc}{\textdom{Loc}}
+\newcommand{\Expr}{\textdom{Expr}}
 
 \newcommand{\cofe}{T}
 \newcommand{\cofeB}{U}
@@ -169,6 +181,7 @@
 \newcommand{\sigax}{A}
 
 \newcommand{\type}{\tau}
+\newcommand{\typeB}{\sigma}
 
 \newcommand{\var}{x}
 \newcommand{\varB}{y}
@@ -184,9 +197,13 @@
 \newcommand{\propB}{Q}
 \newcommand{\propC}{R}
 
-\newcommand{\pred}{\varphi}
-\newcommand{\predB}{\psi}
-\newcommand{\predC}{\zeta}
+% pure propositions
+\newcommand{\pprop}{\phi}
+\newcommand{\ppropB}{\psi}
+
+\newcommand{\pred}{\varPhi}
+\newcommand{\predB}{\Psi}
+\newcommand{\predC}{\Zeta}
 
 \newcommand{\gname}{\gamma}
 \newcommand{\iname}{\iota}
@@ -202,18 +219,19 @@
 \newcommand{\proves}{\vdash}
 \newcommand{\provesIff}{\mathrel{\dashv\vdash}}
 
-\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;}
+\newcommand{\wand}{\mathrel{-\!\!*}}
 
 % oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose...
-\newcommand{\fmapsto}[1][\mathrm{-}]{\xmapsto{#1}}
+\newcommand{\fmapsto}[1][]{\xmapsto{#1}}
 \newcommand{\gmapsto}{\hookrightarrow}%
 \newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%
 
 \NewDocumentCommand\wpre{m O{} m}%
-  {\textlog{wp}_{#2}\spac#1\spac{\{#3\}}}
+  {\textlog{wp}_{#2}\spac#1\spac{\left\{#3\right\}}}
 
-\newcommand{\later}{\mathord{\triangleright}}
-\newcommand{\always}{\Box{}}
+\newcommand{\later}{\mathop{\triangleright}}
+\newcommand{\always}{\mathop{\Box}}
+\newcommand{\pure}{\mathop{\blacksquare}}
 
 %% Invariants and Ghost ownership
 % PDS: Was 0pt inner, 2pt outer.
@@ -222,7 +240,7 @@
 \NewDocumentCommand \boxedassert {O{} m o}{%
 	\tikz[baseline=(m.base)]{
 		%	  \node[rectangle, draw,inner sep=0.8pt,anchor=base,#1] (m) {${#2}\mathstrut$};
-		\node[rectangle,inner sep=0.8pt,outer sep=0.2pt,anchor=base] (m) {${#2}\mathstrut$};
+		\node[rectangle,inner sep=0.8pt,outer sep=0.2pt,anchor=base] (m) {${\,#2\,}\mathstrut$};
 		\draw[#1,boxedassert_border] ($(m.south west) + (0,0.65pt)$) rectangle ($(m.north east) + (0, 0.7pt)$);
 	}\IfNoValueF{#3}{^{\,#3}}%
 }
@@ -256,7 +274,7 @@
 \NewDocumentCommand \vsW {O{} O{}} {\vsGen[#1]{\vsWand}[#2]}
 
 % for now, the update modality looks like a pvs without masks.
-\NewDocumentCommand \upd {} {\mathord{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
+\NewDocumentCommand \upd {} {\mathop{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
 
 
 %% Hoare Triples
@@ -269,12 +287,8 @@
   \setbox1=\hoarescalebox{#1}{\copy0}%
   \setbox2=\hoarescalebox{#2}{\copy0}%
   \copy1{#3}\copy2%
-  \;{#4}\;%
+  \; #4 \;%
   \copy1{#5}\copy2}
-\NewDocumentCommand \hoare {m m m O{}}{
-	\triple\{\}{#1}{#2}{#3}%
-	_{#4}%
-}
 
 \newcommand{\bracket}[4][]{%
   \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}%
@@ -284,6 +298,11 @@
 % \curlybracket[other] x
 \newcommand{\curlybracket}[2][]{\bracket[{#1}]\{\}{#2}}
 \newcommand{\anglebracket}[2][]{\bracket[{#1}]\langle\rangle{#2}}
+
+\NewDocumentCommand \hoare {m m m O{}}{
+	\curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}%
+}
+
 % \hoareV[t] pre c post [mask]
 \NewDocumentCommand \hoareV {O{c} m m m O{}}{
 		{\begin{aligned}[#1]
@@ -321,7 +340,10 @@
 \newcommand{\valB}{w}
 \newcommand{\state}{\sigma}
 \newcommand{\step}{\ra}
+\newcommand{\hstep}{\ra_{\mathsf{h}}}
+\newcommand{\tpstep}{\ra_{\mathsf{tp}}}
 \newcommand{\lctx}{K}
+\newcommand{\Lctx}{\textdom{Ctx}}
 
 \newcommand{\toval}{\mathrm{expr\any to\any val}}
 \newcommand{\ofval}{\mathrm{val\any to\any expr}}
@@ -333,6 +355,8 @@
 
 \newcommand{\cfg}[2]{{#1};{#2}}
 
+\def\fill#1[#2]{#1 {[}\, #2\,{]} }
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % STANDARD DERIVED CONSTRUCTIONS
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -383,12 +407,11 @@
 \newcommand{\stsfstep}[1]{\xrightarrow{#1}}
 \newcommand{\stsftrans}[1]{\stsfstep{#1}^{*}}
 
-
 \tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}]
 \tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}]
 
 %% Stored Propositions
 \newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}}
 
-
 \endinput
+
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 354d342f7ee9349ebfa9712cdfe2823299527071..77f010aea51e00b57c53b7b06e066feeb8debae4 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -96,7 +96,7 @@ The following assertion states that an invariant with name $\iname$ exists and m
 Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
 \[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \]
 Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
-We use $\top$ as symbol for the largest possible mask, $\mathbb N$.
+We use $\top$ as symbol for the largest possible mask, $\mathbb N$, and $\bot$ for the smallest possible mask $\emptyset$.
 We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$.
 %
 View updates satisfy the following basic proof rules:
@@ -230,10 +230,10 @@ The following rules can all be derived inside the DC logic:
 {\mask_1 \subseteq \mask_2 \and \vctx,\var:\textlog{val}\mid\prop \proves \propB}
 {\vctx\mid\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}}
 
-\infer[pvs-wp]
+\infer[vup-wp]
 {}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
 
-\infer[wp-pvs]
+\infer[wp-vup]
 {}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
 
 \infer[wp-atomic]
@@ -409,7 +409,7 @@ All we need to know is that this name is \emph{different} from the names of othe
 Keeping track of the $n^2$ mutual inequalities that arise with $n$ invariants quickly gets in the way of the actual proof.
 
 To solve this issue, instead of remembering the exact name picked for an invariant, we will keep track of the \emph{namespace} the invariant was allocated in.
-Namesapces are sets of invariants, following a tree-like structure:
+Namespaces are sets of invariants, following a tree-like structure:
 Think of the name of an invariant as a sequence of identifiers, much like a fully qualified Java class name.
 A \emph{namespace} $\namesp$ then is like a Java package: it is a sequence of identifiers that we think of as \emph{containing} all invariant names that begin with this sequence. For example, \texttt{org.mpi-sws.iris} is a namespace containing the invariant name \texttt{org.mpi-sws.iris.heap}.
 
@@ -434,7 +434,7 @@ We can now derive the following rules (this involves unfolding the definition of
 \begin{mathpar}
   \axiomH{inv-persist}{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop}
 
-  \axiomH{inv-alloc}{\later\prop \proves \pvs[\bot] \knowInv\namesp\prop}
+  \axiomH{inv-alloc}{\later\prop \proves \pvs[\emptyset] \knowInv\namesp\prop}
 
   \inferH{inv-open}
   {\namesp \subseteq \mask}
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index 71db1619931284c0285b8252ce106204cdb6ad25..6eb603694a60ebdcb491764909b68d5363b5891e 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -87,6 +87,7 @@ Section proof.
     rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
     wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
   Qed.
+
 End proof.
 
 Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
diff --git a/prelude/list.v b/prelude/list.v
index b96edfdc932616582df580d060c2a4aa16927024..c8af713f336f94f9896f192378695f4999573466 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -2234,7 +2234,12 @@ Section Forall_Exists.
   Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l.
   Proof. intro. destruct (Forall_Exists_dec dec l); intuition. Qed.
   Lemma not_Exists_Forall l : ¬Exists P l → Forall (not ∘ P) l.
-  Proof. by destruct (Forall_Exists_dec (λ x, swap_if (decide (P x))) l). Qed.
+  Proof.
+    (* TODO: Coq 8.6 needs type annotation here, Coq 8.5 did not.
+       Should we report this? *)
+    by destruct (@Forall_Exists_dec (not ∘ P) _
+        (λ x : A, swap_if (decide (P x))) l).
+  Qed.
   Global Instance Forall_dec l : Decision (Forall P l) :=
     match Forall_Exists_dec dec l with
     | left H => left H
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index e1dd6e66995336ed3e90cae049635e1300cc657e..1eb1c336b806fc6ecb1270195cae65d8c539226e 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -38,8 +38,8 @@ Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
 Proof.
   iIntros (Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
   { iPureIntro. eapply reducible_not_val, (Hsafe inhabitant). }
-  iIntros (σ1) "Hσ". iApply pvs_intro'; [set_solver|iIntros "Hclose"].
-  iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+  iIntros (σ1) "Hσ". iVs (pvs_intro_mask' E ∅) as "Hclose"; first set_solver.
+  iVsIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
   destruct (Hstep σ1 e2 σ2 efs); auto; subst.
   iVs "Hclose"; iVsIntro. iFrame "Hσ". iApply "H"; auto.
 Qed.
@@ -53,7 +53,7 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (Hatomic ?) "[Hσ H]". iApply (wp_lift_step E _ e1).
-  iApply pvs_intro'; [set_solver|iIntros "Hclose"].
+  iVs (pvs_intro_mask' E ∅) as "Hclose"; first set_solver. iVsIntro.
   iExists σ1. iFrame "Hσ"; iSplit; eauto.
   iNext; iIntros (e2 σ2 efs) "[% Hσ]".
   edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 62de7e675a7c276c1ba2a9c1544b1e17739372f6..06b91c92cac4b5e3d07ec34e55bfd8a7b98037d0 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -52,7 +52,8 @@ Section ndisjoint.
   Lemma ndot_ne_disjoint N x y : x ≠ y → N .@ x ⊥ N .@ y.
   Proof.
     intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq.
-    intros [qx ->] [qy]. by intros [= ?%encode_inj]%list_encode_suffix_eq.
+    intros [qx ->] [qy Hqy].
+    revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq.
   Qed.
 
   Lemma ndot_preserve_disjoint_l N E x : nclose N ⊥ E → nclose (N .@ x) ⊥ E.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 2f6fb5c0a21a9b0d9d1c1dbd4b20f3b21fae50b0..945213d419dd2fcef1ca0d79f6751a5564658594 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -99,6 +99,8 @@ Proof. intros P Q; apply pvs_mono. Qed.
 
 Lemma pvs_intro E P : P ={E}=> P.
 Proof. iIntros "HP". by iApply rvs_pvs. Qed.
+Lemma pvs_intro_mask' E1 E2 : E2 ⊆ E1 → True ⊢ |={E1,E2}=> |={E2,E1}=> True.
+Proof. exact: pvs_intro_mask. Qed.
 Lemma pvs_except_last E1 E2 P : (|={E1,E2}=> â—‡ P) ={E1,E2}=> P.
 Proof. by rewrite {1}(pvs_intro E2 P) except_last_pvs pvs_trans. Qed.
 
@@ -109,11 +111,6 @@ Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
 Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=> Q.
 Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
 
-Lemma pvs_intro' E1 E2 P : E2 ⊆ E1 → ((|={E2,E1}=> True) -★ P) ={E1,E2}=> P.
-Proof.
-  iIntros (?) "Hw". iApply pvs_wand_l. iFrame. by iApply pvs_intro_mask.
-Qed.
-
 Lemma pvs_trans_frame E1 E2 E3 P Q :
   ((Q ={E2,E3}=★ True) ★ |={E1,E2}=> (Q ★ P)) ={E1,E3}=> P.
 Proof.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 0e8244c0b6fc88865e3d0d3562330ef98592387a..fc1e4de7e513cdf0b79d8c52dc7b489836ddb5cd 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -96,7 +96,7 @@ Proof.
   { iDestruct "Hv" as (v) "[% Hv]". iExists v; iSplit; first done.
     iApply ("HΦ" with "==>[-]"). by iApply (pvs_mask_mono E1 _). }
   iSplit; [done|]; iIntros (σ1) "Hσ".
-  iApply (pvs_trans _ E1); iApply pvs_intro'; auto. iIntros "Hclose".
+  iVs (pvs_intro_mask' E2 E1) as "Hclose"; first done.
   iVs ("H" $! σ1 with "Hσ") as "[$ H]".
   iVsIntro. iNext. iIntros (e2 σ2 efs Hstep).
   iVs ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index c63a655e1b9d3f06b9c3c6886ea170f0e8580b4d..9941b50efd827ebcdb84161f6e05c189b8e87cff 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -834,7 +834,7 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
     | ESelName ?p ?H :: ?Hs =>
        iRevert H; go Hs;
        let H' :=
-         match p with true => constr:[IAlwaysElim (IName H)] | false => H end in
+         match p with true => constr:([IAlwaysElim (IName H)]) | false => H end in
        iIntros H'
     end in
   iElaborateSelPat Hs go.
diff --git a/tests/atomic.v b/tests/atomic.v
index 72d20913d518166507a89e29b6b223e14a2b78c0..37cee397c9262b59983951007cb6c808664ed369 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -125,18 +125,15 @@ Section user.
       (* open the invariant *)
       iInv N as (x') ">Hl'" "Hclose".
       (* mask magic *)
-      iApply pvs_intro'.
+      iVs (pvs_intro_mask' _ heapN) as "Hclose'".
       { apply ndisj_subseteq_difference; auto. }
-      iIntros "Hvs".
-      iExists x'.
-      iFrame "Hl'".
-      iSplit.
+      iVsIntro. iExists x'. iFrame "Hl'". iSplit.
       + (* provide a way to rollback *)
         iIntros "Hl'".
-        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
+        iVs "Hclose'". iVs ("Hclose" with "[Hl']"); eauto.
       + (* provide a way to commit *)
         iIntros (v) "[Heq Hl']".
-        iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
+        iVs "Hclose'". iVs ("Hclose" with "[Hl']"); eauto.
     - iDestruct "Hincr" as "#HIncr".
       iSplitL; [|iSplitL]; try (iApply wp_wand_r;iSplitL; [by iApply "HIncr"|auto]).
       iIntros (v1 v2) "_ !>".