diff --git a/_CoqProject b/_CoqProject
index 1e919b355c4136038e8ade6bab57d9a8754106b3..a38123baa312aace8c2df7fae0bf4aae302bd0d8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,7 +67,7 @@ program_logic/model.v
 program_logic/adequacy.v
 program_logic/lifting.v
 program_logic/invariants.v
-program_logic/ownership.v
+program_logic/wsat.v
 program_logic/weakestpre.v
 program_logic/pviewshifts.v
 program_logic/hoare.v
@@ -78,6 +78,7 @@ program_logic/ectxi_language.v
 program_logic/ectx_lifting.v
 program_logic/ghost_ownership.v
 program_logic/saved_prop.v
+program_logic/auth.v
 program_logic/sts.v
 program_logic/namespaces.v
 program_logic/boxes.v
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 7d092323629a5b85e1d6e64eac7f9656b3e5a09a..868722836996ce0327a493c7a68489a729b05944 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:
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index a5e84e8d0a15c643fa9c741bd741ad4a8f0234fe..c6e482cbad95c1aa8907dd784d98850beb855a0e 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -1,28 +1,27 @@
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Export heap.
 From iris.algebra Require Import auth.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> irisPreG heap_lang Σ;
-  heap_preG_heap :> inG Σ (authR heapUR)
+  heap_preG_heap :> authG Σ heapUR
 }.
 
 Definition heapΣ : gFunctors :=
-  #[irisΣ heap_lang; GFunctor (constRF (authR heapUR))].
+  #[irisΣ heap_lang; authΣ heapUR].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
-Proof. intros [? ?%subG_inG]%subG_inv. split; apply _. Qed.
+Proof. intros [? ?]%subG_inv. split; apply _. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   (∀ `{heapG Σ}, heap_ctx ⊢ WP e {{ v, ■ φ v }}) →
   adequate e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
-  iVs (own_alloc (● to_heap σ)) as (γ) "Hh".
-  { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
+  iVs (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
+  { exact: to_heap_valid. }
   set (Hheap := HeapG _ _ _ γ).
-  iVs (inv_alloc heapN _ heap_inv with "[-]"); [iNext; iExists σ; by iFrame|].
   iApply (Hwp _). by rewrite /heap_ctx.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 5401d24f4bfbf2f8c7cac3a47e8bfcc9ab5f6e71..5701bd3136556c0a62aa504be5b125c6756ac29b 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -1,7 +1,7 @@
 From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth gmap frac dec_agree.
 From iris.program_logic Require Export invariants ghost_ownership.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat auth.
 From iris.proofmode Require Import tactics.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
@@ -14,28 +14,26 @@ Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
 (** The CMRA we need. *)
 Class heapG Σ := HeapG {
   heapG_iris_inG :> irisG heap_lang Σ;
-  heap_inG :> inG Σ (authR heapUR);
+  heap_inG :> authG Σ heapUR;
   heap_name : gname
 }.
-(** The Functor we need. *)
+
 Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)).
 
 Section definitions.
   Context `{heapG Σ}.
 
   Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
-    own heap_name (â—¯ {[ l := (q, DecAgree v) ]}).
+    auth_own heap_name ({[ l := (q, DecAgree v) ]}).
   Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
   Definition heap_mapsto := proj1_sig heap_mapsto_aux.
   Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
     proj2_sig heap_mapsto_aux.
 
-  Definition heap_inv : iProp Σ := (∃ σ, ownP σ ★ own heap_name (● to_heap σ))%I.
-  Definition heap_ctx : iProp Σ := inv heapN heap_inv.
+  Definition heap_ctx : iProp Σ := auth_ctx heap_name heapN to_heap ownP.
 End definitions.
 
 Typeclasses Opaque heap_ctx heap_mapsto.
-Instance: Params (@heap_inv) 2.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
@@ -79,8 +77,7 @@ Section heap.
 
   Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ★ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
   Proof.
-    by rewrite heap_mapsto_eq
-      -own_op -auth_frag_op op_singleton pair_op dec_agree_idemp.
+    by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
   Qed.
 
   Lemma heap_mapsto_op l q1 q2 v1 v2 :
@@ -89,8 +86,8 @@ Section heap.
     destruct (decide (v1 = v2)) as [->|].
     { by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
     apply (anti_symm (⊢)); last by apply pure_elim_l.
-    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
-    eapply pure_elim; [done|]=> /auth_own_valid /=.
+    rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid.
+    eapply pure_elim; [done|] =>  /=.
     rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros [].
   Qed.
 
@@ -112,14 +109,12 @@ Section heap.
     heap_ctx ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
     iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
-    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
+    iVs (auth_empty heap_name) as "Ha".
+    iVs (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
     iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !==>".
-    iVs (own_update with "Hh") as "[Hh H]".
-    { apply auth_update_alloc,
-        (alloc_singleton_local_update _ l (1%Qp,DecAgree v));
-        by auto using lookup_to_heap_None. }
-    iVs ("Hclose" with "[Hσ Hh]") as "_".
-    { iNext. iExists (<[l:=v]> σ). rewrite to_heap_insert. by iFrame. }
+    iVs ("Hcl" with "* [Hσ]") as "Ha".
+    { iFrame. iPureIntro. rewrite to_heap_insert.
+      eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
     iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
   Qed.
 
@@ -130,11 +125,9 @@ Section heap.
   Proof.
     iIntros (?) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
-    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
     iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
-    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hclose" with "[Hσ Hh]") as "_".
-    { iNext. iExists σ. by iFrame. }
+    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
     by iApply "HΦ".
   Qed.
 
@@ -145,16 +138,12 @@ Section heap.
   Proof.
     iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
-    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
     iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
-    iIntros "{$Hσ} !> Hσ !==>".
-    iVs (own_update_2 with "[$Hh $Hl]") as "[Hh Hl]".
-    { eapply auth_update, singleton_local_update,
-        (exclusive_local_update _ (1%Qp, DecAgree v)); last done.
+    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha".
+    { iFrame. iPureIntro. rewrite to_heap_insert.
+      eapply singleton_local_update, exclusive_local_update; last done.
       by eapply heap_singleton_included'. }
-    iVs ("Hclose" with "[Hσ Hh]") as "_".
-    { iNext. iExists (<[l:=v]>σ). rewrite to_heap_insert. iFrame. }
     by iApply "HΦ".
   Qed.
 
@@ -165,11 +154,9 @@ Section heap.
   Proof.
     iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
-    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
     iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
-    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hclose" with "[Hσ Hh]") as "_".
-    { iNext. iExists σ. by iFrame. }
+    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
     by iApply "HΦ".
   Qed.
 
@@ -180,16 +167,12 @@ Section heap.
   Proof.
     iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
     rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ) ">[Hσ Hh] " "Hclose".
-    iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
+    iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
     iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included.
-    iIntros "{$Hσ} !> Hσ !==>".
-    iVs (own_update_2 with "[$Hh $Hl]") as "[Hh Hl]".
-    { eapply auth_update, singleton_local_update,
-        (exclusive_local_update _ (1%Qp, DecAgree v2)); last done.
+    iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha".
+    { iFrame. iPureIntro. rewrite to_heap_insert.
+      eapply singleton_local_update, exclusive_local_update; last done.
       by eapply heap_singleton_included'. }
-    iVs ("Hclose" with "[Hσ Hh]") as "_".
-    { iNext. iExists (<[l:=v2]>σ). rewrite to_heap_insert. iFrame. }
     by iApply "HΦ".
   Qed.
 End heap.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 278165adb0f0d324b009188c8d92aa6ada6c45ee..917c0002535885440ee3463fcbb9b946834e9340 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
+From iris.program_logic Require Import wsat ectx_lifting. (* for ownP *)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
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/adequacy.v b/program_logic/adequacy.v
index 4b6540a71517af9c68ceca1c731d4a7bcbff075c..96377473f7932fa1bee8d1526db956ceac455b48 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
diff --git a/program_logic/auth.v b/program_logic/auth.v
new file mode 100644
index 0000000000000000000000000000000000000000..81217798b0a2abb9a06c8564ee9a2492db456e2b
--- /dev/null
+++ b/program_logic/auth.v
@@ -0,0 +1,148 @@
+From iris.program_logic Require Export invariants.
+From iris.algebra Require Export auth.
+From iris.algebra Require Import gmap.
+From iris.proofmode Require Import tactics.
+Import uPred.
+
+(* The CMRA we need. *)
+Class authG Σ (A : ucmraT) := AuthG {
+  auth_inG :> inG Σ (authR A);
+  auth_discrete :> CMRADiscrete A;
+}.
+Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].
+
+Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A.
+Proof. intros ?%subG_inG ?. by split. Qed.
+
+Section definitions.
+  Context `{irisG Λ Σ, authG Σ A} {T : Type} (γ : gname).
+
+  Definition auth_own (a : A) : iProp Σ :=
+    own γ (◯ a).
+  Definition auth_inv (f : T → A) (φ : T → iProp Σ) : iProp Σ :=
+    (∃ t, own γ (● f t) ★ φ t)%I.
+  Definition auth_ctx (N : namespace) (f : T → A) (φ : T → iProp Σ) : iProp Σ :=
+    inv N (auth_inv f φ).
+
+  Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own.
+  Proof. solve_proper. Qed.
+  Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
+  Proof. solve_proper. Qed.
+  Global Instance auth_own_timeless a : TimelessP (auth_own a).
+  Proof. apply _. Qed.
+  Global Instance auth_own_persistent a : Persistent a → PersistentP (auth_own a).
+  Proof. apply _. Qed.
+
+  Global Instance auth_inv_ne n :
+    Proper (pointwise_relation T (dist n) ==>
+            pointwise_relation T (dist n) ==> dist n) auth_inv.
+  Proof. solve_proper. Qed.
+  Global Instance auth_inv_proper :
+    Proper (pointwise_relation T (≡) ==>
+            pointwise_relation T (⊣⊢) ==> (⊣⊢)) auth_inv.
+  Proof. solve_proper. Qed.
+  Global Instance auth_ctx_ne N n :
+    Proper (pointwise_relation T (dist n) ==>
+            pointwise_relation T (dist n) ==> dist n) (auth_ctx N).
+  Proof. solve_proper. Qed.
+  Global Instance auth_ctx_proper N :
+    Proper (pointwise_relation T (≡) ==>
+            pointwise_relation T (⊣⊢) ==> (⊣⊢)) (auth_ctx N).
+  Proof. solve_proper. Qed.
+  Global Instance auth_ctx_persistent N f φ : PersistentP (auth_ctx N f φ).
+  Proof. apply _. Qed.
+End definitions.
+
+Typeclasses Opaque auth_own auth_inv auth_ctx.
+Instance: Params (@auth_own) 4.
+Instance: Params (@auth_inv) 5.
+Instance: Params (@auth_ctx) 8.
+
+Section auth.
+  Context `{irisG Λ Σ, authG Σ A}.
+  Context {T : Type} `{!Inhabited T}.
+  Context (f : T → A) (φ : T → iProp Σ).
+  Implicit Types N : namespace.
+  Implicit Types P Q R : iProp Σ.
+  Implicit Types a b : A.
+  Implicit Types t u : T.
+  Implicit Types γ : gname.
+
+  Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b.
+  Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
+
+  Global Instance from_sep_auth_own γ a b1 b2 :
+    FromOp a b1 b2 →
+    FromSep (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
+  Proof. rewrite /FromOp /FromSep=> <-. by rewrite auth_own_op. Qed.
+  Global Instance into_and_auth_own p γ a b1 b2 :
+    IntoOp a b1 b2 →
+    IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
+  Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) auth_own_op. Qed.
+
+  Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
+  Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
+  Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
+  Proof. by rewrite /auth_own own_valid auth_validI. Qed.
+
+  Global Instance auth_own_cmra_homomorphism : CMRAHomomorphism (auth_own γ).
+  Proof. split. apply _. apply auth_own_op. Qed.
+  Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (auth_own γ).
+  Proof. intros a1 a2. apply auth_own_mono. Qed.
+
+  Lemma auth_alloc_strong N E t (G : gset gname) :
+    ✓ (f t) → ▷ φ t ={E}=> ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
+  Proof.
+    iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
+    iVs (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
+    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
+    iVs (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
+    { iNext. rewrite /auth_inv. iExists t. by iFrame. }
+    eauto.
+  Qed.
+
+  Lemma auth_alloc N E t :
+    ✓ (f t) → ▷ φ t ={E}=> ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t).
+  Proof.
+    iIntros (?) "Hφ".
+    iVs (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
+  Qed.
+
+  Lemma auth_empty γ : True =r=> auth_own γ ∅.
+  Proof. by rewrite /auth_own -own_empty. Qed.
+
+  Lemma auth_acc E γ a :
+    ▷ auth_inv γ f φ ★ auth_own γ a ={E}=> ∃ t,
+      ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b,
+      ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E}=★ ▷ auth_inv γ f φ ★ auth_own γ b.
+  Proof.
+    iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own.
+    iDestruct "Hinv" as (t) "[>Hγa Hφ]".
+    iVsIntro. iExists t.
+    iDestruct (own_valid_2 with "[$Hγa $Hγf]") as % [? ?]%auth_valid_discrete_2.
+    iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
+    iVs (own_update_2 with "[$Hγa $Hγf]") as "[Hγa Hγf]".
+    { eapply auth_update; eassumption. }
+    iVsIntro. iFrame. iExists u. iFrame.
+  Qed.
+
+  Lemma auth_open E N γ a :
+    nclose N ⊆ E →
+    auth_ctx γ N f φ ★ auth_own γ a ={E,E∖N}=> ∃ t,
+      ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b,
+      ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E∖N,E}=★ auth_own γ b.
+  Proof.
+    iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
+    (* The following is essentially a very trivial composition of the accessors
+       [auth_acc] and [inv_open] -- but since we don't have any good support
+       for that currently, this gets more tedious than it should, with us having
+       to unpack and repack various proofs.
+       TODO: Make this mostly automatic, by supporting "opening accessors
+       around accessors". *)
+    iVs (auth_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
+    iVsIntro. iExists t. iFrame. iIntros (u b) "H".
+    iVs ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iVs ("Hclose" with "Hinv").
+  Qed.
+End auth.
+
+Arguments auth_open {_ _ _ _} [_] {_} [_] _ _ _ _ _ _ _.
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index b43ead95ec2738b2795f44de64500150735a1ecd..7d329558b564a425bb82efff655babbb2abcf7d1 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -1,6 +1,6 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 
 Section wp.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 08b7407aeafa4ff9a41f59e2199bf451ec8b75bc..8fe284f2401764adb8f6a741f76ae90f8fe28e93 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export pviewshifts.
 From iris.program_logic Require Export namespaces.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics coq_tactics intro_patterns.
 Import uPred.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index da791e981fcfdd125d79a3b104902ba5f7a45acc..9a1d0ad9f4655dad4ff76e719afeee0e79961d27 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Export upred_big_op.
 From iris.proofmode Require Import tactics.
 
@@ -35,8 +35,8 @@ Lemma wp_lift_pure_step E Φ e1 :
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
-  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.
@@ -51,7 +51,7 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
 Proof.
   iIntros (Hatomic ?) "[Hσ H]".
   iApply (wp_lift_step E _ e1); eauto using reducible_not_val.
-  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 cf2070e49ed4146c360b060e4bbed93cd1e375e3..945213d419dd2fcef1ca0d79f6751a5564658594 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export iris.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Import upred_big_op gmap.
 From iris.proofmode Require Import tactics classes.
 Import uPred.
@@ -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 9c8d93f85ad43402a71c975d9ec62f2bae3f6950..fc1e4de7e513cdf0b79d8c52dc7b489836ddb5cd 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export pviewshifts.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics classes.
@@ -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/program_logic/ownership.v b/program_logic/wsat.v
similarity index 100%
rename from program_logic/ownership.v
rename to program_logic/wsat.v
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 0b978bab802c84dd816be2935cbb01692c1d8457..37cee397c9262b59983951007cb6c808664ed369 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
+From iris.program_logic Require Export hoare weakestpre pviewshifts.
 From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics.
@@ -41,7 +41,9 @@ Section atomic.
   Arguments atomic_triple {_} _ _ _ _.
 End atomic.
 
+(* TODO: Importing in the middle of the file is bad practice. *)
 From iris.heap_lang Require Export lang proofmode notation.
+From iris.heap_lang.lib Require Import par.
 
 Section incr.
   Context `{!heapG Σ} (N : namespace).
@@ -92,7 +94,6 @@ Section incr.
   Qed.
 End incr.
 
-From iris.heap_lang.lib Require Import par.
 
 Section user.
   Context `{!heapG Σ, !spawnG Σ} (N : namespace).
@@ -124,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) "_ !>".
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 3a1a31fd2762dff8e943396b72faadb504082e62..bccc4848ca9410f450ead0a1f93a5427d0a2a7d6 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -2,7 +2,7 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import adequacy.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import wsat.
 From iris.heap_lang Require Import proofmode notation.
 
 Section LiftingTests.