diff --git a/ProofMode.md b/ProofMode.md
index 59846cef5fe77688ae9fb15a7bda9dc511c72212..8137c2c6c140c5e1b9d0885e161e4cfa169b62f4 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -32,12 +32,18 @@ Context management
 - `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
 - `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
   implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
+- `iSpecialize pm_trm as #` : instantiate universal quantifiers and eliminate
+  implications/wands of a hypothesis whose conclusion is persistent. In this
+  case, all hypotheses can be used for proving the premises, as well as for
+  the resulting goal.
 - `iPoseProof pm_trm as "H"` : put `pm_trm` into the context as a new hypothesis
   `H`.
 - `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and
   put `P` in the context of the original goal. The specialization pattern
-  `spat` specifies which hypotheses will be consumed by proving `P` and the
+  `spat` specifies which hypotheses will be consumed by proving `P`. The
   introduction pattern `ipat` specifies how to eliminate `P`.
+- `iAssert P with "spat" as %cpat` : assert `P` and eliminate it using the Coq
+  introduction pattern `cpat`.
 
 Introduction of logical connectives
 -----------------------------------
@@ -60,12 +66,17 @@ Elimination of logical connectives
 ----------------------------------
 
 - `iExFalso` : Ex falso sequitur quod libet.
-- `iDestruct pm_trm as (x1 ... xn) "spat1 ... spatn"` : elimination of
-  existential quantifiers using Coq introduction patterns `x1 ... xn` and
-  elimination of object level connectives using the proof mode introduction
-  patterns `ipat1 ... ipatn`.
+- `iDestruct pm_trm as (x1 ... xn) "ipat"` : elimination of existential
+  quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
+  object level connectives using the proof mode introduction pattern `ipat`.
+  In case all branches of `ipat` start with an `#` (moving the hypothesis to the
+  persistent context) or `%` (moving the hypothesis to the pure Coq context),
+  one can use all hypotheses for proving the premises of `pm_trm`, as well as
+  for proving the resulting goal.
 - `iDestruct pm_trm as %cpat` : elimination of a pure hypothesis using the Coq
-  introduction pattern `cpat`.
+  introduction pattern `cpat`. When using this tactic, all hypotheses can be
+  used for proving the premises of `pm_trm`, as well as for proving the
+  resulting goal.
 
 Separating logic specific tactics
 ---------------------------------
@@ -180,9 +191,9 @@ so called specification patterns to express this splitting:
 - `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
   is a primitive view shift, in which case the view shift will be kept in the
   goal of the premise too.
-- `[#]` : This pattern can be used when eliminating `P -★ Q` when either `P` or
-  `Q` is persistent. In this case, all hypotheses are available in the goal for
-  the premise as none will be consumed.
+- `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
+  persistent. Using this pattern, all hypotheses are available in the goal for
+  `P`, as well the remaining goal.
 - `[%]` : This pattern can be used when eliminating `P -★ Q` when `P` is pure.
   It will generate a Coq goal for `P` and does not consume any hypotheses.
 - `*` : instantiate all top-level universal quantifiers with meta variables.
diff --git a/_CoqProject b/_CoqProject
index 54a1a2d1594cda76579af944d8b8b6cc6dd24295..ed943035c2fbdf70e573ad252b73cdf188482637 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -62,6 +62,7 @@ algebra/updates.v
 algebra/local_updates.v
 algebra/gset.v
 algebra/coPset.v
+algebra/double_negation.v
 program_logic/model.v
 program_logic/adequacy.v
 program_logic/lifting.v
diff --git a/algebra/auth.v b/algebra/auth.v
index 5e7a7633c7344a2dc87b44fe15e16653ef71d776..e8d25bfd6b0c65fb87aedbbc6fc4a48d3c2cd9ba 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -95,9 +95,10 @@ Proof.
   split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
   intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
 Qed.
-Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} authoritative x.
+
+Lemma authoritative_validN n x : ✓{n} x → ✓{n} authoritative x.
 Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_validN n (x : auth A) : ✓{n} x → ✓{n} auth_own x.
+Lemma auth_own_validN n x : ✓{n} x → ✓{n} auth_own x.
 Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
 
 Lemma auth_valid_discrete `{CMRADiscrete A} x :
@@ -111,6 +112,14 @@ Proof.
   setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
 Qed.
 
+Lemma authoritative_valid  x : ✓ x → ✓ authoritative x.
+Proof. by destruct x as [[[]|]]. Qed.
+Lemma auth_own_valid `{CMRADiscrete A} x : ✓ x → ✓ auth_own x.
+Proof.
+  rewrite auth_valid_discrete.
+  destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
+Qed.
+
 Lemma auth_cmra_mixin : CMRAMixin (auth A).
 Proof.
   apply cmra_total_mixin.
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 689433b1925d783da5f5386726015598a2c88478..f9c689fadcccc4760305980702c452aa0343de9f 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -342,6 +342,8 @@ Global Instance cmra_included_trans: Transitive (@included A _ _).
 Proof.
   intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2). by rewrite assoc -Hy -Hz.
 Qed.
+Lemma cmra_valid_included x y : ✓ y → x ≼ y → ✓ x.
+Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_valid_op_l. Qed.
 Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x.
 Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
 Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x.
@@ -984,6 +986,10 @@ Section prod_unit.
 
   Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ∅) ⋅ (∅, y).
   Proof. by rewrite pair_op left_id right_id. Qed.
+
+  Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
+    (x, y) = (x, ∅) ⋅ (∅, y).
+  Proof. unfold_leibniz. apply pair_split. Qed.
 End prod_unit.
 
 Arguments prodUR : clear implicits.
diff --git a/algebra/double_negation.v b/algebra/double_negation.v
new file mode 100644
index 0000000000000000000000000000000000000000..0e9145c72b4870f39b105db64ac83ddfc0134b46
--- /dev/null
+++ b/algebra/double_negation.v
@@ -0,0 +1,380 @@
+From iris.algebra Require Import upred.
+Import upred.
+
+(* In this file we show that the rvs can be thought of a kind of
+   step-indexed double-negation when our meta-logic is classical *)
+
+(* To define this, we need a way to talk about iterated later modalities: *)
+Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M :=
+  Nat.iter n uPred_later P.
+Instance: Params (@uPred_laterN) 2.
+Notation "â–·^ n P" := (uPred_laterN n P)
+  (at level 20, n at level 9, right associativity,
+   format "â–·^ n  P") : uPred_scope.
+
+Definition uPred_nnvs {M} (P: uPred M) : uPred M :=
+  ∀ n, (P -★ ▷^n False) -★ ▷^n False.
+
+Notation "|=n=> Q" := (uPred_nnvs Q)
+  (at level 99, Q at level 200, format "|=n=>  Q") : uPred_scope.
+Notation "P =n=> Q" := (P ⊢ |=n=> Q)
+  (at level 99, Q at level 200, only parsing) : C_scope.
+Notation "P =n=★ Q" := (P -★ |=n=> Q)%I
+  (at level 99, Q at level 200, format "P  =n=★  Q") : uPred_scope.
+
+(* Our goal is to prove that:
+  (1) |=n=> has (nearly) all the properties of the |=r=> modality that are used in Iris
+  (2) If our meta-logic is classical, then |=n=> and |=r=> are equivalent
+*)
+
+Section rvs_nnvs.
+Context {M : ucmraT}.
+Implicit Types φ : Prop.
+Implicit Types P Q : uPred M.
+Implicit Types A : Type.
+Implicit Types x : M.
+Import uPred.
+
+(* Helper lemmas about iterated later modalities *)
+Lemma laterN_big n a x φ: ✓{n} x →  a ≤ n → (▷^a (■ φ))%I n x → φ.
+Proof.
+  induction 2 as [| ?? IHle].
+  - induction a; repeat (rewrite //= || uPred.unseal). 
+    intros Hlater. apply IHa; auto using cmra_validN_S.
+    move:Hlater; repeat (rewrite //= || uPred.unseal). 
+  - intros. apply IHle; auto using cmra_validN_S.
+    eapply uPred_closed; eauto using cmra_validN_S.
+Qed.
+
+Lemma laterN_small n a x φ: ✓{n} x →  n < a → (▷^a (■ φ))%I n x.
+Proof.
+  induction 2.
+  - induction n as [| n IHn]; [| move: IHn];
+      repeat (rewrite //= || uPred.unseal).
+    naive_solver eauto using cmra_validN_S.
+  - induction n as [| n IHn]; [| move: IHle];
+      repeat (rewrite //= || uPred.unseal).
+    red; rewrite //=. intros.
+    eapply (uPred_closed _ _ (S n)); eauto using cmra_validN_S.
+Qed.
+
+(* It is easy to show that most of the basic properties of rvs that
+   are used throughout Iris hold for nnvs. 
+
+   In fact, the first three properties that follow hold for any
+   modality of the form (- -★ Q) -★ Q for arbitrary Q. The situation
+   here is slightly different, because nnvs is of the form 
+   ∀ n, (- -★ (Q n)) -★ (Q n), but the proofs carry over straightforwardly.
+
+ *)
+
+Lemma nnvs_intro P : P =n=> P.
+Proof. apply forall_intro=>?. apply wand_intro_l, wand_elim_l. Qed.
+Lemma nnvs_mono P Q : (P ⊢ Q) → (|=n=> P) =n=> Q.
+Proof.
+  intros HPQ. apply forall_intro=>n.
+  apply wand_intro_l.  rewrite -{1}HPQ.
+  rewrite /uPred_nnvs (forall_elim n).
+  apply wand_elim_r.
+Qed.
+Lemma nnvs_frame_r P R : (|=n=> P) ★ R =n=> P ★ R.
+Proof.
+  apply forall_intro=>n. apply wand_intro_r.
+  rewrite (comm _ P) -wand_curry.
+  rewrite /uPred_nnvs (forall_elim n).
+  by rewrite -assoc wand_elim_r wand_elim_l.
+Qed.
+Lemma nnvs_ownM_updateP x (Φ : M → Prop) :
+  x ~~>: Φ → uPred_ownM x =n=> ∃ y, ■ Φ y ∧ uPred_ownM y.
+Proof. 
+  intros Hrvs. split. rewrite /uPred_nnvs. repeat uPred.unseal. 
+  intros n y ? Hown a.
+  red; rewrite //= => n' yf ??.
+  inversion Hown as (x'&Hequiv).
+  edestruct (Hrvs n' (Some (x' â‹… yf))) as (y'&?&?); eauto.
+  { by rewrite //= assoc -(dist_le _ _ _ _ Hequiv). }
+  case (decide (a ≤ n')).
+  - intros Hle Hwand.
+    exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' (y' â‹… x'))); eauto.
+    * rewrite comm -assoc. done. 
+    * rewrite comm -assoc. done. 
+    * eexists. split; eapply uPred_mono; red; rewrite //=; eauto.
+  - intros; assert (n' < a). omega.
+    move: laterN_small. uPred.unseal.
+    naive_solver.
+Qed.
+
+(* However, the transitivity property seems to be much harder to
+   prove. This is surprising, because transitivity does hold for 
+   modalities of the form (- -★ Q) -★ Q. What goes wrong when we quantify
+   now over n? 
+ *)
+
+Remark nnvs_trans P: (|=n=> |=n=> P) ⊢ (|=n=> P).
+Proof.
+  rewrite /uPred_nnvs.
+  apply forall_intro=>a. apply wand_intro_l.
+  rewrite (forall_elim a).
+  rewrite (nnvs_intro (P -★ _)).
+  rewrite /uPred_nnvs.
+  (* Oops -- the exponents of the later modality don't match up! *)
+Abort.
+
+(* Instead, we will need to prove this in the model. We start by showing that 
+   nnvs is the limit of a the following sequence:
+
+   (- -★ False) - ★ False,
+   (- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False,
+   (- -★ ▷^2 False) - ★ ▷^2 False ∧ (- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False,
+   ...
+
+   Then, it is easy enough to show that each of the uPreds in this sequence
+   is transitive. It turns out that this implies that nnvs is transitive. *)
+   
+
+(* The definition of the sequence above: *)
+Fixpoint uPred_nnvs_k {M} k (P: uPred M) : uPred M :=
+  ((P -★ ▷^k False) -★ ▷^k False) ∧
+  match k with 
+    O => True
+  | S k' => uPred_nnvs_k k' P
+  end.
+
+Notation "|=n=>_ k Q" := (uPred_nnvs_k k Q)
+  (at level 99, k at level 9, Q at level 200, format "|=n=>_ k  Q") : uPred_scope.
+
+
+(* One direction of the limiting process is easy -- nnvs implies nnvs_k for each k *)
+Lemma nnvs_trunc1 k P: (|=n=> P) ⊢ |=n=>_k P.
+Proof.
+  induction k. 
+  - rewrite /uPred_nnvs_k /uPred_nnvs. 
+    rewrite (forall_elim 0) //= right_id //.
+  - simpl. apply and_intro; auto.
+    rewrite /uPred_nnvs. 
+    rewrite (forall_elim (S k)) //=.
+Qed.
+
+Lemma nnvs_k_elim n k P: n ≤ k → ((|=n=>_k P) ★ (P -★ (▷^n False)) ⊢  (▷^n False))%I.
+Proof.
+  induction k.
+  - inversion 1; subst; rewrite //= ?right_id. apply wand_elim_l.
+  - inversion 1; subst; rewrite //= ?right_id.
+    * rewrite and_elim_l. apply wand_elim_l.
+    * rewrite and_elim_r IHk //.
+Qed.
+
+Lemma nnvs_k_unfold k P:
+  (|=n=>_(S k) P) ⊣⊢ ((P -★ (▷^(S k) False)) -★ (▷^(S k) False)) ∧ (|=n=>_k P).
+Proof. done.  Qed.
+Lemma nnvs_k_unfold' k P n x:
+  (|=n=>_(S k) P)%I n x ↔ (((P -★ (▷^(S k) False)) -★ (▷^(S k) False)) ∧ (|=n=>_k P))%I n x.
+Proof. done.  Qed.
+
+Lemma nnvs_k_weaken k P: (|=n=>_(S k) P) ⊢ |=n=>_k P.
+Proof. by rewrite nnvs_k_unfold and_elim_r. Qed.
+
+(* Now we are ready to show nnvs is the limit -- ie, for each k, it is within distance k
+   of the kth term of the sequence *)
+Lemma nnvs_nnvs_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
+  split; intros n' x Hle Hx. split.
+  - by apply (nnvs_trunc1 k).
+  - revert n' x Hle Hx; induction k; intros n' x Hle Hx;
+      rewrite ?nnvs_k_unfold' /uPred_nnvs.
+    * rewrite //=. unseal.
+      inversion Hle; subst.
+      intros (HnnP&_) n k' x' ?? HPF.
+      case (decide (k' < n)).
+      ** move: laterN_small; uPred.unseal; naive_solver.
+      ** intros. exfalso. eapply HnnP; eauto.
+         assert (n ≤ k'). omega.
+         intros n'' x'' ???.
+         specialize (HPF n'' x''). exfalso.
+         eapply laterN_big; last (unseal; eauto).
+         eauto. omega.
+    * inversion Hle; subst.
+      ** unseal. intros (HnnP&HnnP_IH) n k' x' ?? HPF.
+         case (decide (k' < n)).
+         *** move: laterN_small; uPred.unseal; naive_solver.
+         *** intros. exfalso. assert (n ≤ k'). omega.
+             assert (n = S k ∨ n < S k) as [->|] by omega.
+             **** eapply laterN_big; eauto; unseal. eapply HnnP; eauto.
+             **** move:nnvs_k_elim. unseal. intros Hnnvsk. 
+                  eapply laterN_big; eauto. unseal.
+                  eapply (Hnnvsk n k); first omega; eauto.
+                  exists x, x'. split_and!; eauto. eapply uPred_closed; eauto.
+                  eapply cmra_validN_op_l; eauto.
+      ** intros HP. eapply IHk; auto.
+         move:HP. unseal. intros (?&?); naive_solver.
+Qed.
+
+(* nnvs_k has a number of structural properties, including transitivity *)
+Lemma nnvs_k_intro k P: P ⊢ (|=n=>_k P).
+Proof.
+  induction k; rewrite //= ?right_id.
+  - apply wand_intro_l. apply wand_elim_l.
+  - apply and_intro; auto. 
+    apply wand_intro_l. apply wand_elim_l.
+Qed.
+
+Lemma nnvs_k_mono k P Q: (P ⊢ Q) → (|=n=>_k P) ⊢ (|=n=>_k Q).
+Proof.
+  induction k; rewrite //= ?right_id=>HPQ. 
+  - do 2 (apply wand_mono; auto).
+  - apply and_mono; auto; do 2 (apply wand_mono; auto).
+Qed.
+Instance nnvs_k_mono' k: Proper ((⊢) ==> (⊢)) (@uPred_nnvs_k M k).
+Proof. by intros P P' HP; apply nnvs_k_mono. Qed.
+
+Instance nnvs_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnvs_k M k).
+Proof. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed.
+Lemma nnvs_k_proper k P Q: (P ⊣⊢ Q) → (|=n=>_k P) ⊣⊢ (|=n=>_k Q).
+Proof. intros HP; apply (anti_symm (⊢)); eapply nnvs_k_mono; by rewrite HP. Qed.
+Instance nnvs_k_proper' k: Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_nnvs_k M k).
+Proof. by intros P P' HP; apply nnvs_k_proper. Qed.
+
+Lemma nnvs_k_trans k P: (|=n=>_k |=n=>_k P) ⊢ (|=n=>_k P).
+Proof.
+  revert P.
+  induction k; intros P.
+  - rewrite //= ?right_id. apply wand_intro_l. 
+    rewrite {1}(nnvs_k_intro 0 (P -★ False)%I) //= ?right_id. apply wand_elim_r. 
+  - rewrite {2}(nnvs_k_unfold k P).
+    apply and_intro.
+    * rewrite (nnvs_k_unfold k P). rewrite and_elim_l.
+      rewrite nnvs_k_unfold. rewrite and_elim_l.
+      apply wand_intro_l. 
+      rewrite {1}(nnvs_k_intro (S k) (P -★ ▷^(S k) (False)%I)).
+      rewrite nnvs_k_unfold and_elim_l. apply wand_elim_r.
+    * do 2 rewrite nnvs_k_weaken //.
+Qed.
+
+Lemma nnvs_trans P : (|=n=> |=n=> P) =n=> P.
+Proof.
+  split=> n x ? Hnn.
+  eapply nnvs_nnvs_k_dist in Hnn; eauto.
+  eapply (nnvs_k_ne (n) n ((|=n=>_(n) P)%I)) in Hnn; eauto;
+    [| symmetry; eapply nnvs_nnvs_k_dist].
+  eapply nnvs_nnvs_k_dist; eauto.
+  by apply nnvs_k_trans.
+Qed.
+
+(* Now that we have shown nnvs has all of the desired properties of
+   rvs, we go further and show it is in fact equivalent to rvs! The
+   direction from rvs to nnvs is similar to the proof of
+   nnvs_ownM_updateP *)
+
+Lemma rvs_nnvs P: (|=r=> P) ⊢ |=n=> P.
+Proof.
+  split. rewrite /uPred_nnvs. repeat uPred.unseal. intros n x ? Hrvs a.
+  red; rewrite //= => n' yf ??.
+  edestruct Hrvs as (x'&?&?); eauto.
+  case (decide (a ≤ n')).
+  - intros Hle Hwand.
+    exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' x')); eauto.
+    * rewrite comm. done. 
+    * rewrite comm. done. 
+  - intros; assert (n' < a). omega.
+    move: laterN_small. uPred.unseal.
+    naive_solver.
+Qed.
+
+(* However, the other direction seems to need a classical axiom: *)
+Section classical.
+Context (not_all_not_ex: ∀ (P : M → Prop), ¬ (∀ n : M, ¬ P n) → ∃ n : M, P n).
+Lemma nnvs_rvs P:  (|=n=> P) ⊢ (|=r=> P).
+Proof.
+  rewrite /uPred_nnvs.
+  split. uPred.unseal; red; rewrite //=.
+  intros n x ? Hforall k yf Hle ?.
+  apply not_all_not_ex.
+  intros Hfal.
+  specialize (Hforall k k).
+  eapply laterN_big; last (uPred.unseal; red; rewrite //=; eapply Hforall);
+    eauto.
+  red; rewrite //= => n' x' ???.
+  case (decide (n' = k)); intros.
+  - subst. exfalso. eapply Hfal. rewrite (comm op); eauto.
+  - assert (n' < k). omega.
+    move: laterN_small. uPred.unseal. naive_solver.
+Qed.
+End classical.
+
+(* We might wonder whether we can prove an adequacy lemma for nnvs. We could combine
+   the adequacy lemma for rvs with the previous result to get adquacy for nnvs, but 
+   this would rely on the classical axiom we needed to prove the equivalence! Can
+   we establish adequacy without axioms? Unfortunately not, because adequacy for 
+   nnvs would imply double negation elimination, which is classical: *)
+
+Lemma nnvs_dne φ: True ⊢ (|=n=> (■(¬¬ φ → φ)): uPred M)%I.
+Proof.
+  rewrite /uPred_nnvs. apply forall_intro=>n.
+  apply wand_intro_l. rewrite ?right_id. 
+  assert (∀ φ, ¬¬¬¬φ → ¬¬φ) by naive_solver.
+  assert (Hdne: ¬¬ (¬¬φ → φ)) by naive_solver.
+  split. unseal. intros n' ?? Hvs.
+  case (decide (n' < n)).
+  - intros. move: laterN_small. unseal. naive_solver.
+  - intros. assert (n ≤ n'). omega. 
+    exfalso. specialize (Hvs n' ∅).
+    eapply Hdne. intros Hfal.
+    eapply laterN_big; eauto. 
+    unseal. rewrite right_id in Hvs *; naive_solver.
+Qed.
+
+(* Nevertheless, we can prove a weaker form of adequacy (which is equvialent to adequacy
+   under classical axioms) directly without passing through the proofs for rvs: *)
+Lemma adequacy_helper1 P n k x:
+  ✓{S n + k} x → ¬¬ (Nat.iter (S n) (λ P, |=n=> ▷ P)%I P (S n + k) x) 
+            → ¬¬ (∃ x', ✓{n + k} (x') ∧ Nat.iter n (λ P, |=n=> ▷ P)%I P (n + k) (x')).
+Proof.
+  revert k P x. induction n.
+  - rewrite /uPred_nnvs. unseal=> k P x Hx Hf1 Hf2.
+    eapply Hf1. intros Hf3.
+    eapply (laterN_big (S k) (S k)); eauto.
+    specialize (Hf3 (S k) (S k) ∅). rewrite right_id in Hf3 *. unseal.
+    intros Hf3. eapply Hf3; eauto.
+    intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
+    unseal. 
+    assert (n' < S k ∨ n' = S k) as [|] by omega.
+    * intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall. 
+      eapply Hsmall; eauto.
+    * subst. intros. exfalso. eapply Hf2. exists x'. split; eauto using cmra_validN_S.
+  - intros k P x Hx. rewrite ?Nat_iter_S_r. 
+    replace (S (S n) + k) with (S n + (S k)) by omega.
+    replace (S n + k) with (n + (S k)) by omega.
+    intros. eapply IHn. replace (S n + S k) with (S (S n) + k) by omega. eauto.
+    rewrite ?Nat_iter_S_r. eauto.
+Qed.
+
+Lemma adequacy_helper2 P n k x:
+  ✓{S n + k} x → ¬¬ (Nat.iter (S n) (λ P, |=n=> ▷ P)%I P (S n + k) x) 
+            → ¬¬ (∃ x', ✓{k} (x') ∧ Nat.iter 0 (λ P, |=n=> ▷ P)%I P k (x')).
+Proof.
+  revert x. induction n.
+  - specialize (adequacy_helper1 P 0). rewrite //=. naive_solver.
+  - intros ?? Hfal%adequacy_helper1; eauto using cmra_validN_S.
+    intros Hfal'. eapply Hfal. intros (x''&?&?).
+    eapply IHn; eauto.
+Qed.
+
+Lemma adequacy φ n : (True ⊢ Nat.iter n (λ P, |=n=> ▷ P) (■ φ)) → ¬¬ φ.
+Proof.
+  cut (∀ x, ✓{S n} x → Nat.iter n (λ P, |=n=> ▷ P)%I (■ φ)%I (S n) x → ¬¬φ).
+  { intros help H. eapply (help ∅); eauto using ucmra_unit_validN.
+    eapply H; try unseal; eauto using ucmra_unit_validN. red; rewrite //=. }
+  destruct n.
+  - rewrite //=; unseal; auto.
+  - intros ??? Hfal.
+    eapply (adequacy_helper2 _ n 1); (replace (S n + 1) with (S (S n)) by omega); eauto.
+    unseal. intros (x'&?&Hphi). simpl in *.
+    eapply Hfal. auto.
+Qed.
+
+(* Open question:
+
+   Do the basic properties of the |=r=> modality (rvs_intro, rvs_mono, rvs_trans, rvs_frame_r,
+      rvs_ownM_updateP, and adequacy) uniquely characterize |=r=>?
+*)
+
+End rvs_nnvs.
\ No newline at end of file
diff --git a/heap_lang/lib/barrier/barrier.v b/heap_lang/lib/barrier/barrier.v
index b9ebaf60b3ffb601d1e1430c81b02760b515d31b..f30edf8dd558439eebaf3b3fe627785182f561a3 100644
--- a/heap_lang/lib/barrier/barrier.v
+++ b/heap_lang/lib/barrier/barrier.v
@@ -1,7 +1,7 @@
 From iris.heap_lang Require Export notation.
 
-Definition newbarrier : val := λ: <>, ref #0.
-Definition signal : val := λ: "x", "x" <- #1.
+Definition newbarrier : val := λ: <>, ref #false.
+Definition signal : val := λ: "x", "x" <- #true.
 Definition wait : val :=
-  rec: "wait" "x" := if: !"x" = #1 then #() else "wait" "x".
+  rec: "wait" "x" := if: !"x" then #() else "wait" "x".
 Global Opaque newbarrier signal wait.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index b427bb5b36f6322cdc4a199b011508b9e2798e62..9be41c4dea243d726b15cc6f08ceade668add3c3 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -28,7 +28,7 @@ Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ :=
     ▷ (P -★ [★ set] i ∈ I, Ψ i) ★ [★ set] i ∈ I, saved_prop_own i (Ψ i))%I.
 
 Coercion state_to_val (s : state) : val :=
-  match s with State Low _ => #0 | State High _ => #1 end.
+  match s with State Low _ => #false | State High _ => #true end.
 Arguments state_to_val !_ / : simpl nomatch.
 
 Definition state_to_prop (s : state) (P : iProp Σ) : iProp Σ :=
@@ -145,7 +145,7 @@ Proof.
     { iSplit; first done. iNext. rewrite {2}/barrier_inv /=. by iFrame. }
     iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "==>[Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
-    iVsIntro. wp_op=> ?; simplify_eq; wp_if.
+    iVsIntro. wp_if.
     iApply ("IH" with "Hγ [HQR] HΦ"). auto.
   - (* a High state: the comparison succeeds, and we perform a transition and
     return to the client *)
@@ -157,7 +157,7 @@ Proof.
     { iSplit; [iPureIntro; by eauto using wait_step|].
       iNext. rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame. auto. }
     iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
-    iVsIntro. wp_op=> ?; simplify_eq/=; wp_if.
+    iVsIntro. wp_if.
     iVsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
 Qed.
 
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 1a91d7e7576e97668309ad7ef1add0f4c2c502a4..1c94a2ecf1812892890d9edef749a68bd7796f36 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -9,7 +9,7 @@ Definition par : val :=
     let: "handle" := spawn (Fst "fs") in
     let: "v2" := Snd "fs" #() in
     let: "v1" := join "handle" in
-    Pair "v1" "v2".
+    ("v1", "v2").
 Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
 Global Opaque par.
 
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 28fa844df19a5ae1408ebaf7b0909941ff4b199d..d4994cd762b91c116fb7ff35a469ee55bfa672cb 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -1,124 +1,108 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.program_logic Require Import auth.
 From iris.proofmode Require Import invariants.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import gset.
+From iris.algebra Require Import auth gset.
 From iris.heap_lang.lib Require Export lock.
 Import uPred.
 
 Definition wait_loop: val :=
-  rec: "wait_loop" "x" "lock" :=
-    let: "o" := !(Fst "lock") in
+  rec: "wait_loop" "x" "lk" :=
+    let: "o" := !(Fst "lk") in
     if: "x" = "o"
       then #() (* my turn *)
-      else "wait_loop" "x" "lock".
+      else "wait_loop" "x" "lk".
 
 Definition newlock : val := λ: <>, ((* owner *) ref #0, (* next *) ref #0).
 
 Definition acquire : val :=
-  rec: "acquire" "lock" :=
-    let: "n" := !(Snd "lock") in
-    if: CAS (Snd "lock") "n" ("n" + #1)
-      then wait_loop "n" "lock"
-      else "acquire" "lock".
-
-Definition release : val :=
-  rec: "release" "lock" :=
-    let: "o" := !(Fst "lock") in
-    if: CAS (Fst "lock") "o" ("o" + #1)
-      then #()
-      else "release" "lock".
+  rec: "acquire" "lk" :=
+    let: "n" := !(Snd "lk") in
+    if: CAS (Snd "lk") "n" ("n" + #1)
+      then wait_loop "n" "lk"
+      else "acquire" "lk".
+
+Definition release : val := λ: "lk",
+  (Fst "lk") <- !(Fst "lk") + #1.
 
 Global Opaque newlock acquire release wait_loop.
 
 (** The CMRAs we need. *)
-Class tlockG Σ := TlockG {
-   tlock_G :> authG Σ (gset_disjUR nat);
-   tlock_exclG  :> inG Σ (exclR unitC)
-}.
+Class tlockG Σ :=
+  tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))).
 Definition tlockΣ : gFunctors :=
-  #[authΣ (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
+  #[ GFunctor (constRF (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat)))) ].
 
 Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
-Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
+Proof. by intros ?%subG_inG. Qed.
 
 Section proof.
   Context `{!heapG Σ, !tlockG Σ} (N : namespace).
 
-  Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp Σ :=
-    (gs = GSet (seq_set 0 n))%I.
-
-  Definition lock_inv (γ1 γ2: gname) (lo ln: loc) (R : iProp Σ) : iProp Σ :=
-    (∃ (o n: nat),
-       lo ↦ #o ★ ln ↦ #n ★
-       auth_inv γ1 (tickets_inv n) ★
-       ((own γ2 (Excl ()) ★ R) ∨ auth_own γ1 (GSet {[ o ]})))%I.
+  Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
+    (∃ o n : nat,
+      lo ↦ #o ★ ln ↦ #n ★
+      own γ (● (Excl' o, GSet (seq_set 0 n))) ★
+      ((own γ (◯ (Excl' o, ∅)) ★ R) ∨ own γ (◯ (∅, GSet {[ o ]}))))%I.
 
-  Definition is_lock (γs: gname * gname) (l: val) (R: iProp Σ) : iProp Σ :=
-    (∃ (lo ln: loc),
+  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
+    (∃ lo ln : loc,
        heapN ⊥ N ∧ heap_ctx ∧
-       l = (#lo, #ln)%V ∧ inv N (lock_inv (fst γs) (snd γs) lo ln R))%I.
+       lk = (#lo, #ln)%V ∧ inv N (lock_inv γ lo ln R))%I.
 
-  Definition issued (γs: gname * gname) (l : val) (x: nat) (R : iProp Σ) : iProp Σ :=
-    (∃ (lo ln: loc),
+  Definition issued (γ : gname) (lk : val) (x : nat) (R : iProp Σ) : iProp Σ :=
+    (∃ lo ln: loc,
        heapN ⊥ N ∧ heap_ctx ∧
-       l = (#lo, #ln)%V ∧ inv N (lock_inv (fst γs) (snd γs) lo ln R) ∧
-       auth_own (fst γs) (GSet {[ x ]}))%I.
+       lk = (#lo, #ln)%V ∧ inv N (lock_inv γ lo ln R) ∧
+       own γ (◯ (∅, GSet {[ x ]})))%I.
 
-  Definition locked (γs: gname * gname) : iProp Σ := own (snd γs) (Excl ())%I.
+  Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, ∅)))%I.
 
-  Global Instance lock_inv_ne n γ1 γ2 lo ln :
-    Proper (dist n ==> dist n) (lock_inv γ1 γ2 lo ln).
+  Global Instance lock_inv_ne n γ lo ln :
+    Proper (dist n ==> dist n) (lock_inv γ lo ln).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_ne γs n l : Proper (dist n ==> dist n) (is_lock γs l).
+  Global Instance is_lock_ne γ n lk : Proper (dist n ==> dist n) (is_lock γ lk).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_persistent γs l R : PersistentP (is_lock γs l R).
+  Global Instance is_lock_persistent γ lk R : PersistentP (is_lock γ lk R).
   Proof. apply _. Qed.
-  Global Instance locked_timeless γs : TimelessP (locked γs).
+  Global Instance locked_timeless γ : TimelessP (locked γ).
   Proof. apply _. Qed.
 
-  Lemma locked_exclusive (γs: gname * gname) : (locked γs ★ locked γs ⊢ False)%I.
-  Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
+  Lemma locked_exclusive (γ : gname) : (locked γ ★ locked γ ⊢ False)%I.
+  Proof.
+    iIntros "[H1 H2]". iDestruct "H1" as (o1) "H1". iDestruct "H2" as (o2) "H2".
+    iCombine "H1" "H2" as "H". iDestruct (own_valid with "H") as %[[] _].
+  Qed.
 
   Lemma newlock_spec (R : iProp Σ) Φ :
     heapN ⊥ N →
-    heap_ctx ★ R ★ (∀ lk γs, is_lock γs lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
+    heap_ctx ★ R ★ (∀ lk γ, is_lock γ lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
   Proof.
     iIntros (HN) "(#Hh & HR & HΦ)". rewrite /newlock /=.
     wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
-    iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
-    iVs (own_alloc_strong (Auth (Excl' ∅) ∅) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
-    iVs (inv_alloc N _ (lock_inv γ1 γ2 lo ln R) with "[-HΦ]").
-    - iNext. rewrite /lock_inv.
-      iExists 0%nat, 0%nat.
-      iFrame.
-      iSplitL "Hγ1".
-      + rewrite /auth_inv.
-        iExists (GSet ∅).
-        by iFrame.
-      + iLeft. by iFrame.
-    - iVsIntro.
-      iApply ("HΦ" $! (#lo, #ln)%V (γ1, γ2)).
-      iExists lo, ln.
-      iSplit; by eauto.
+    iVs (own_alloc (● (Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
+    { by rewrite -auth_both_op. }
+    iVs (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
+    { iNext. rewrite /lock_inv.
+      iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
+    iVsIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
   Qed.
 
-  Lemma wait_loop_spec γs l x R (Φ : val → iProp Σ) :
-    issued γs l x R ★ (locked γs -★ R -★ Φ #()) ⊢ WP wait_loop #x l {{ Φ }}.
+  Lemma wait_loop_spec γ lk x R (Φ : val → iProp Σ) :
+    issued γ lk x R ★ (locked γ -★ R -★ Φ #()) ⊢ WP wait_loop #x lk {{ Φ }}.
   Proof.
     iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
     iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
-    iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
+    iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
     wp_load. destruct (decide (x = o)) as [->|Hneq].
     - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
-      + iVs ("Hclose" with "[Hlo Hln Hainv Ht]").
+      + iVs ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
         { iNext. iExists o, n. iFrame. eauto. }
         iVsIntro. wp_let. wp_op=>[_|[]] //.
         wp_if. iVsIntro.
-        iApply ("HΦ" with "[-HR] HR"). eauto.
+        iApply ("HΦ" with "[-HR] HR"). rewrite /locked; eauto.
       + iExFalso. iCombine "Ht" "Haown" as "Haown".
-        iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
+        iDestruct (own_valid with "Haown") as % [_ ?%gset_disj_valid_op].
         set_solver.
     - iVs ("Hclose" with "[Hlo Hln Ha]").
       { iNext. iExists o, n. by iFrame. }
@@ -126,64 +110,72 @@ Section proof.
       wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
   Qed.
 
-  Lemma acquire_spec γs l R (Φ : val → iProp Σ) :
-    is_lock γs l R ★ (locked γs -★ R -★ Φ #()) ⊢ WP acquire l {{ Φ }}.
+  Lemma acquire_spec γ lk R (Φ : val → iProp Σ) :
+    is_lock γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }}.
   Proof.
     iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
     iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
     iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
-    wp_load. iVs ("Hclose" with "[Hlo Hln Ha]").
+    wp_load. iVs ("Hclose" with "[Hlo Hln Ha]") as "_".
     { iNext. iExists o, n. by iFrame. }
     iVsIntro. wp_let. wp_proj. wp_op.
     wp_bind (CAS _ _ _).
-    iInv N as (o' n') "[Hlo' [Hln' [Hainv Haown]]]" "Hclose".
+    iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)" "Hclose".
     destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
     - wp_cas_suc.
-      iDestruct "Hainv" as (s) "[Ho %]"; subst.
-      iVs (own_update with "Ho") as "Ho".
-      { eapply auth_update_no_frag, (gset_disj_alloc_empty_local_update n).
-        rewrite elem_of_seq_set; omega. }
-      iDestruct "Ho" as "[Hofull Hofrag]".
-      iVs ("Hclose" with "[Hlo' Hln' Haown Hofull]").
-      { rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
-        rewrite -(seq_set_S_union_L 0).
-        iNext. iExists o', (S n)%nat.
-        rewrite Nat2Z.inj_succ -Z.add_1_r.
-        iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
+      iVs (own_update with "Hauth") as "Hauth".
+      { eapply (auth_update_no_frag _ (∅, _)), prod_local_update,
+          (gset_disj_alloc_empty_local_update n); [done|].
+        rewrite elem_of_seq_set. omega. }
+      rewrite pair_op left_id_L. iDestruct "Hauth" as "[Hauth Hofull]".
+      rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
+      rewrite -(seq_set_S_union_L 0).
+      iVs ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
+      { iNext. iExists o', (S n).
+        rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
       iVsIntro. wp_if.
-      iApply (wait_loop_spec γs (#lo, #ln)).
-      iSplitR "HΦ"; last by auto.
-      rewrite /issued /auth_own; eauto 10.
+      iApply (wait_loop_spec γ (#lo, #ln)).
+      iFrame "HΦ". rewrite /issued; eauto 10.
     - wp_cas_fail.
-      iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
+      iVs ("Hclose" with "[Hlo' Hln' Hauth Haown]").
       { iNext. iExists o', n'. by iFrame. }
       iVsIntro. wp_if. by iApply "IH".
   Qed.
 
-  Lemma release_spec γs l R (Φ : val → iProp Σ):
-    is_lock γs l R ★ locked γs ★ R ★ Φ #() ⊢ WP release l {{ Φ }}.
+  Lemma release_spec γ lk R (Φ : val → iProp Σ):
+    is_lock γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}.
   Proof.
-    iIntros "(Hl & Hγ & HR & HΦ)". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
-    iLöb as "IH". wp_rec. subst. wp_proj. wp_bind (! _)%E.
-    iInv N as (o n) "[Hlo [Hln Hr]]" "Hclose".
-    wp_load. iVs ("Hclose" with "[Hlo Hln Hr]").
+    iIntros "(Hl & Hγ & HR & HΦ)".
+    iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
+    iDestruct "Hγ" as (o) "Hγo".
+    rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
+    iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
+    wp_load.
+    iAssert (o' = o)%I with "[#]" as "%"; subst.
+    { iCombine "Hγo" "Hauth" as "Hγo".
+      by iDestruct (own_valid with "Hγo") (* FIXME: this is horrible *)
+        as %[[[[?|] ?] [=]%leibniz_equiv_iff] ?]%auth_valid_discrete. }
+    iVs ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
     { iNext. iExists o, n. by iFrame. }
-    iVsIntro. wp_let. wp_bind (CAS _ _ _ ).
-    wp_proj. wp_op.
-    iInv N as (o' n') "[Hlo' [Hln' Hr]]" "Hclose".
-    destruct (decide (#o' = #o))%V as [[= ->%Nat2Z.inj ] | Hneq].
-    - wp_cas_suc.
-      iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]".
-      + iExFalso. iCombine "Hγ" "Ho" as "Ho".
-        iDestruct (own_valid with "#Ho") as %[].
-      + iVs ("Hclose" with "[Hlo' Hln' HR Hγ Hainv]").
-        { iNext. iExists (o + 1)%nat, n'%nat.
-          iFrame. rewrite Nat2Z.inj_add.
-          iFrame. iLeft; by iFrame. }
-        iVsIntro. by wp_if.
-    - wp_cas_fail. iVs ("Hclose" with "[Hlo' Hln' Hr]").
-      { iNext. iExists o', n'. by iFrame. }
-      iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
+    iVsIntro. wp_op.
+    iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
+    wp_store.
+    iAssert (o' = o)%I with "[#]" as "%"; subst.
+    { iCombine "Hγo" "Hauth" as "Hγo".
+      by iDestruct (own_valid with "Hγo")
+        as %[[[[?|] ?] [=]%leibniz_equiv_iff] ?]%auth_valid_discrete. }
+    iDestruct "Haown" as "[[Hγo' _]|?]".
+    { iCombine "Hγo" "Hγo'" as "Hγo".
+      iDestruct (own_valid with "Hγo") as %[[] ?]. }
+    iCombine "Hauth" "Hγo" as "Hauth".
+    iVs (own_update with "Hauth") as "Hauth".
+    { rewrite pair_split_L. apply: (auth_update _ _ (Excl' (S o), _)). (* FIXME: apply is slow *)
+      apply prod_local_update, reflexivity; simpl.
+      by apply option_local_update, exclusive_local_update. }
+    rewrite -pair_split_L. iDestruct "Hauth" as "[Hauth Hγo]".
+    iVs ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last auto.
+    iNext. iExists (S o), n'.
+    rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
   Qed.
 End proof.
 
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 6fc3ed36e8abd2e03e2a5eca67c5093adf31a545..8abbf502b397e7b8f8387e293fdb0e9575ac03fd 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -550,3 +550,19 @@ Lemma Qp_div_2 x : (x / 2 + x / 2 = x)%Qp.
 Proof.
   change 2%positive with (2 * 1)%positive. by rewrite Qp_div_S, Qp_div_1.
 Qed.
+
+Lemma Qp_lower_bound q1 q2 : ∃ q q1' q2', (q1 = q + q1' ∧ q2 = q + q2')%Qp.
+Proof.
+  revert q1 q2. cut (∀ q1 q2 : Qp, (q1 ≤ q2)%Qc →
+    ∃ q q1' q2', (q1 = q + q1' ∧ q2 = q + q2')%Qp).
+  { intros help q1 q2.
+    destruct (Qc_le_dec q1 q2) as [LE|LE%Qclt_nge%Qclt_le_weak]; [by eauto|].
+    destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto. }
+  intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp.
+  assert (0 < q2 - q1 / 2)%Qc as Hq2'.
+  { eapply Qclt_le_trans; [|by apply Qcplus_le_mono_r, Hq].
+    replace (q1 - q1 / 2)%Qc with (q1 * (1 - 1/2))%Qc by ring.
+    replace 0%Qc with (0 * (1-1/2))%Qc by ring. by apply Qcmult_lt_compat_r. }
+  exists (mk_Qp (q2 - q1 / 2%Z) Hq2'). split; [by rewrite Qp_div_2|].
+  apply Qp_eq; simpl. ring.
+Qed.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index b2480ac7ed9d2e702f47e0b82cc2640da20b790b..5569939f7e2b865bfcc8675ecc0276f5cb8f6a3f 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -134,7 +134,7 @@ Proof.
   rewrite pvs_eq in HI;
     iVs (HI with "HI [Hw HE]") as "> (_ & _ & H)"; first by iFrame.
   iDestruct "H" as (σ2') "[Hσf %]".
-  iDestruct (ownP_agree σ2 σ2' with "[#]") as %<-. by iFrame. eauto.
+  iDestruct (ownP_agree σ2 σ2' with "[-]") as %<-. by iFrame. eauto.
 Qed.
 End adequacy.
 
diff --git a/program_logic/auth.v b/program_logic/auth.v
index a56f54d5b2e6533e2b15122dc6cb32db4e925339..99231ad4b0cf0597d3aba06bb77d80627a66e656 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -98,7 +98,7 @@ Section auth.
   Proof.
     iIntros (?) "(#? & >Hγf)". rewrite /auth_ctx /auth_own.
     iInv N as (a') "[>Hγ Hφ]" "Hclose". iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (own_valid with "#Hγ") as % [[af Ha'] ?]%auth_valid_discrete.
+    iDestruct (own_valid with "Hγ") as % [[af Ha'] ?]%auth_valid_discrete.
     simpl in Ha'; rewrite ->(left_id _ _) in Ha'; setoid_subst.
     iVsIntro. iExists af; iFrame "Hφ"; iSplit; first done.
     iIntros (b) "[% Hφ]".
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 97a46c231fdb095347c590bfbef6efd07a22353e..29c34b6b8d517dfad1da31caee94b0bb39434cba 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -118,8 +118,7 @@ Proof.
   iDestruct (big_sepM_delete _ f _ false with "Hf")
     as "[[Hγ' #[HγΦ ?]] ?]"; first done.
   iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
-  iDestruct (box_own_auth_agree γ b false with "[#]")
-    as "%"; subst; first by iFrame.
+  iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
   iSplitL "Hγ"; last iSplit.
   - iExists false; eauto.
   - iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_sepM_delete.
@@ -153,8 +152,7 @@ Proof.
   iDestruct (big_sepM_later _ f with "Hf") as "Hf".
   iDestruct (big_sepM_delete _ f with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
-  iDestruct (box_own_auth_agree γ b true with "[#]")
-    as %?; subst; first by iFrame.
+  iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
   iFrame "HQ".
   iVs (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ Hγ']"; first by iFrame.
   iVs ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
@@ -189,8 +187,7 @@ Proof.
     iAlways; iIntros (γ b ?) "(Hγ' & #$ & #$)".
     assert (true = b) as <- by eauto.
     iInv N as (b) "(>Hγ & _ & HΦ)" "Hclose".
-    iDestruct (box_own_auth_agree γ b true with "[#]")
-      as "%"; subst; first by iFrame.
+    iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
     iVs (box_own_auth_update γ true true false with "[Hγ Hγ']")
       as "[Hγ $]"; first by iFrame.
     iVs ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 1dcd9a8b070e1170939df6d504072b4e0e9efd20..16ef16d2ab251d56e2c66554f9021767519c8542 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -20,7 +20,7 @@ Lemma wp_lift_step E Φ e1 :
 Proof.
   iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
   iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
-  iDestruct (ownP_agree σ1 σ1' with "[#]") as %<-; first by iFrame.
+  iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
   iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
   iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
   iApply "H"; eauto.
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 5badaaded9f02f7c05dec7d870b63a6f430e1a61..51093e7f59107e6b2b1c7e122d9a9c350951ab98 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -43,41 +43,27 @@ Proof. apply nclose_subseteq with x, encode_nclose. Qed.
 Lemma nclose_infinite N : ¬set_finite (nclose N).
 Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
 
-Instance ndisjoint : Disjoint namespace := λ N1 N2,
-  ∃ N1' N2', N1' `suffix_of` N1 ∧ N2' `suffix_of` N2 ∧
-             length N1' = length N2' ∧ N1' ≠ N2'.
-Typeclasses Opaque ndisjoint.
+Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 ⊥ nclose N2.
 
 Section ndisjoint.
   Context `{Countable A}.
   Implicit Types x y : A.
 
-  Global Instance ndisjoint_symmetric : Symmetric ndisjoint.
-  Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed.
-
   Lemma ndot_ne_disjoint N x y : x ≠ y → N .@ x ⊥ N .@ y.
-  Proof. intros. exists (N .@ x), (N .@ y); rewrite ndot_eq; naive_solver. Qed.
-
-  Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → N1 .@ x ⊥ N2.
   Proof.
-    intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
-    split_and?; try done; []. rewrite ndot_eq. by apply suffix_of_cons_r.
+    intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq.
+    intros [qx ->] [qy]. by intros [= ?%encode_inj]%list_encode_suffix_eq.
   Qed.
 
-  Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ N2 .@ x .
-  Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
+  Lemma ndot_preserve_disjoint_l N E x : nclose N ⊥ E → nclose (N .@ x) ⊥ E.
+  Proof. intros. pose proof (nclose_subseteq N x). set_solver. Qed.
 
-  Lemma ndisj_disjoint N1 N2 : N1 ⊥ N2 → nclose N1 ⊥ nclose N2.
-  Proof.
-    intros (N1' & N2' & [N1'' ->] & [N2'' ->] & Hl & Hne) p.
-    rewrite nclose_eq /nclose.
-    rewrite !elem_coPset_suffixes; intros [q ->] [q' Hq]; destruct Hne.
-    by rewrite !list_encode_app !assoc in Hq; apply list_encode_suffix_eq in Hq.
-  Qed.
+  Lemma ndot_preserve_disjoint_r N E x : E ⊥ nclose N → E ⊥ nclose (N .@ x).
+  Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
 
-  Lemma ndisj_subseteq_difference N1 N2 E :
-    N1 ⊥ N2 → nclose N1 ⊆ E → nclose N1 ⊆ E ∖ nclose N2.
-  Proof. intros ?%ndisj_disjoint. set_solver. Qed.
+  Lemma ndisj_subseteq_difference N E F :
+    E ⊥ nclose N → E ⊆ F → E ⊆ F ∖ nclose N.
+  Proof. set_solver. Qed.
 End ndisjoint.
 
 (* The hope is that registering these will suffice to solve most goals
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index aa42399a2fbe6873124186e7564ef59ca25d4d8b..b6f3ad902b6bd9784c805b54cd0a4b0303f5ed82 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -89,7 +89,7 @@ Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed
 Lemma ownE_op' E1 E2 : E1 ⊥ E2 ∧ ownE (E1 ∪ E2) ⊣⊢ ownE E1 ★ ownE E2.
 Proof.
   iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
-  iIntros "HE". iDestruct (ownE_disjoint with "#HE") as %?.
+  iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?.
   iSplit; first done. iApply ownE_op; by try iFrame.
 Qed.
 Lemma ownE_singleton_twice i : ownE {[i]} ★ ownE {[i]} ⊢ False.
@@ -104,7 +104,7 @@ Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
 Lemma ownD_op' E1 E2 : E1 ⊥ E2 ∧ ownD (E1 ∪ E2) ⊣⊢ ownD E1 ★ ownD E2.
 Proof.
   iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
-  iIntros "HE". iDestruct (ownD_disjoint with "#HE") as %?.
+  iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?.
   iSplit; first done. iApply ownD_op; by try iFrame.
 Qed.
 Lemma ownD_singleton_twice i : ownD {[i]} ★ ownD {[i]} ⊢ False.
@@ -132,19 +132,19 @@ Qed.
 Lemma ownI_open i P : wsat ★ ownI i P ★ ownE {[i]} ⊢ wsat ★ ▷ P ★ ownD {[i]}.
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
-  iDestruct (invariant_lookup I i P with "[#]") as (Q) "[% #HPQ]"; [by iFrame|].
+  iDestruct (invariant_lookup I i P with "[-]") as (Q) "[% #HPQ]"; [by iFrame|].
   iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|?] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
     iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI"; eauto.
-  - iDestruct (ownE_singleton_twice with "[#]") as %[]. by iFrame.
+  - iDestruct (ownE_singleton_twice with "[-]") as %[]. by iFrame.
 Qed.
 Lemma ownI_close i P : wsat ★ ownI i P ★ ▷ P ★ ownD {[i]} ⊢ wsat ★ ownE {[i]}.
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
-  iDestruct (invariant_lookup with "[#]") as (Q) "[% #HPQ]"; first by iFrame.
+  iDestruct (invariant_lookup with "[-]") as (Q) "[% #HPQ]"; first by iFrame.
   iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
-  - iDestruct (ownD_singleton_twice with "[#]") as %[]. by iFrame.
+  - iDestruct (ownD_singleton_twice with "[-]") as %[]. by iFrame.
   - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
 Qed.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 586777c6fe9cbab329b0d3c0b461027510738365..ef4f749d170b80d7cab3392f4ba4659c1f2b0e0d 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -13,7 +13,7 @@ Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.
 Arguments pvs {_ _ _} _ _ _%I.
 Instance: Params (@pvs) 5.
 
-Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
+Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q)
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }=>  Q") : uPred_scope.
 Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I
@@ -22,7 +22,7 @@ Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I
 Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q)
   (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
 
-Notation "|={ E }=> Q" := (pvs E E Q%I)
+Notation "|={ E }=> Q" := (pvs E E Q)
   (at level 99, E at level 50, Q at level 200,
    format "|={ E }=>  Q") : uPred_scope.
 Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I
@@ -31,9 +31,12 @@ Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I
 Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
   (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
 
-Notation "|={ E1 , E2 }â–·=> Q" := (|={E1%I,E2%I}=> â–· |={E2,E1}=> Q)%I
+Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }â–·=>  Q") : uPred_scope.
+Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "|={ E }â–·=>  Q") : uPred_scope.
 
 Section pvs.
 Context `{irisG Λ Σ}.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 4693dc29d71f4f8da0476dcbdff5c6f20e6081bd..a27c28ce626975b1f37f8fa5642ef1b9c4a85445 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -95,7 +95,7 @@ Section sts.
   Proof.
     iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own.
     iDestruct "Hinv" as (s) "[>Hγ Hφ]".
-    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "#Hγ") as %Hvalid.
+    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ") as %Hvalid.
     assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
     assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
     rewrite sts_op_auth_frag //.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 02f910142868835e4e4fa17e90ca33621ceb3ea5..d7b188265fdc0767296004247b2ecc4db74eef99 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -4,14 +4,22 @@ From iris.proofmode Require Import pviewshifts invariants.
 Definition vs `{irisG Λ Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P → |={E1,E2}=> Q))%I.
 Arguments vs {_ _ _} _ _ _%I _%I.
+
 Instance: Params (@vs) 5.
-Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
+Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
   (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : uPred_scope.
 Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
   (at level 99, E at level 50, Q at level 200,
    format "P  ={ E }=>  Q") : uPred_scope.
 
+Notation "P ={ E1 , E2 }â–·=> Q" := (P ={E1,E2}=> â–· |={E2,E1}=> Q)%I
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "P ={ E1 , E2 }â–·=>  Q") : uPred_scope.
+Notation "P ={ E }â–·=> Q" := (P ={E,E}â–·=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P ={ E }â–·=>  Q") : uPred_scope.
+
 Section vs.
 Context `{irisG Λ Σ}.
 Implicit Types P Q R : iProp Σ.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 0d116ac97199e239e0466e730b17191de8e793a0..0917c2769e0a226e24ef15b77f57714312f8d3ab 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -488,7 +488,7 @@ Proof.
   by rewrite always_if_elim assoc !wand_elim_r.
 Qed.
 
-Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
+Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
   IntoWand R P1 P2 → FromPure P1 φ →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
@@ -498,24 +498,31 @@ Proof.
   by rewrite right_id (into_wand R) -(from_pure P1) // wand_True wand_elim_r.
 Qed.
 
-Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
+Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
-  IntoWand R P1 P2 →
+  IntoWand R P1 P2 → PersistentP P1 →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
-  (Δ' ⊢ P1) → (PersistentP P1 ∨ PersistentP P2) →
-  (Δ'' ⊢ Q) → Δ ⊢ Q.
+  (Δ' ⊢ P1) → (Δ'' ⊢ Q) → Δ ⊢ Q.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
+  rewrite envs_lookup_sound //.
+  rewrite -(idemp uPred_and (envs_delete _ _ _)).
+  rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
+  rewrite envs_simple_replace_sound' //; simpl.
+  rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
+  by rewrite wand_elim_r.
+Qed.
+
+Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
+  envs_lookup j Δ = Some (q,P) →
+  (Δ ⊢ R) → PersistentP R →
+  envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' →
+  (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ?? HP1 [?|?] <-.
-  - rewrite envs_lookup_sound //.
-    rewrite -(idemp uPred_and (envs_delete _ _ _)).
-    rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
-    rewrite envs_simple_replace_sound' //; simpl.
-    rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
-    by rewrite wand_elim_r.
-  - rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
-    rewrite envs_simple_replace_sound //; simpl.
-    rewrite (sep_elim_r _ (_ -★ _)) right_id (into_wand R) always_if_elim.
-    by rewrite wand_elim_l always_and_sep_l -{1}(always_if_always q P2) wand_elim_r.
+  intros ? HR ?? <-.
+  rewrite -(idemp uPred_and Δ) {1}HR always_and_sep_l.
+  rewrite envs_replace_sound //; simpl.
+  by rewrite right_id assoc (sep_elim_l R) always_always wand_elim_r.
 Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index ac49db83957e8c257589e6b1940a64d5773e6f60..f2feecb4417f6276a4754a3d77781b213b67d0fc 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -19,6 +19,15 @@ Inductive intro_pat :=
   | IAll : intro_pat
   | IClear : list (bool * string) → intro_pat. (* true = frame, false = clear *)
 
+Fixpoint intro_pat_persistent (p : intro_pat) :=
+  match p with
+  | IPureElim => true
+  | IAlwaysElim _ => true
+  | ILaterElim p => intro_pat_persistent p
+  | IList pps => forallb (forallb intro_pat_persistent) pps
+  | _ => false
+  end.
+
 Module intro_pat.
 Inductive token :=
   | TName : string → token
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index 03f6d40f97dbd8b10b6edb5d3c8f8009f4c67b25..d72706b2f9a4c9a8eb93decd5176250bf6d3b677 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -6,7 +6,7 @@ Inductive spec_pat :=
   | SGoal : spec_goal_kind → bool → list string → spec_pat
   | SGoalPersistent : spec_pat
   | SGoalPure : spec_pat
-  | SName : bool → string → spec_pat (* first arg = persistent *)
+  | SName : string → spec_pat
   | SForall : spec_pat.
 
 Module spec_pat.
@@ -44,13 +44,12 @@ Inductive state :=
 Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
   match ts with
   | [] => Some (rev k)
-  | TName s :: ts => parse_go ts (SName false s :: k)
+  | TName s :: ts => parse_go ts (SName s :: k)
   | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
   | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
   | TBracketL :: ts => parse_goal ts GoalStd false [] k
   | TVs :: TBracketL :: ts => parse_goal ts GoalVs false [] k
   | TVs :: ts => parse_go ts (SGoal GoalVs true [] :: k)
-  | TPersistent :: TName s :: ts => parse_go ts (SName true s :: k)
   | TForall :: ts => parse_go ts (SForall :: k)
   | _ => None
   end
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 3db566b13d7826a9f01b40c78c1764159af5dd5a..19db5a773733508f916ce8098ca1ea8535ae35dd 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -152,7 +152,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
     lazymatch pats with
     | [] => idtac
     | SForall :: ?pats => try (iSpecializeArgs H1 (hcons _ _)); go H1 pats
-    | SName false ?H2 :: ?pats =>
+    | SName ?H2 :: ?pats =>
        eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
          [env_cbv; reflexivity || fail "iSpecialize:" H2 "not found"
          |env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
@@ -160,30 +160,17 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
           let Q := match goal with |- IntoWand ?P ?Q _ => Q end in
           apply _ || fail "iSpecialize: cannot instantiate" P "with" Q
          |env_cbv; reflexivity|go H1 pats]
-    | SName true ?H2 :: ?pats =>
-       eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
-         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
-         |solve_to_wand H1
-         |env_cbv; reflexivity
-         |iExact H2 || fail "iSpecialize:" H2 "not found or wrong type"
-         |let Q1 := match goal with |- PersistentP ?Q1 ∨ _ => Q1 end in
-          let Q2 := match goal with |- _ ∨ PersistentP ?Q2 => Q2 end in
-          first [left; apply _ | right; apply _]
-            || fail "iSpecialize:" Q1 "nor" Q2 "persistent"
-         |go H1 pats]
     | SGoalPersistent :: ?pats =>
-       eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
+       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
+         |let Q := match goal with |- PersistentP ?Q => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
          |env_cbv; reflexivity
          |(*goal*)
-         |let Q1 := match goal with |- PersistentP ?Q1 ∨ _ => Q1 end in
-          let Q2 := match goal with |- _ ∨ PersistentP ?Q2 => Q2 end in
-          first [left; apply _ | right; apply _]
-            || fail "iSpecialize:" Q1 "nor" Q2 "persistent"
          |go H1 pats]
     | SGoalPure :: ?pats =>
-       eapply tac_specialize_pure with _ H1 _ _ _ _ _;
+       eapply tac_specialize_assert_pure with _ H1 _ _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |let Q := match goal with |- FromPure ?Q _ => Q end in
@@ -204,11 +191,37 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          |go H1 pats]
     end in let pats := spec_pat.parse pat in go H pats.
 
-Tactic Notation "iSpecialize" open_constr(t) :=
-  match t with
-  | ITrm ?H ?xs ?pat => iSpecializeArgs H xs; iSpecializePat H pat
+(* p = whether the conclusion of the specialized term is persistent. It can
+either be a Boolean or an introduction pattern, which will be coerced in true
+when it only contains `#` or `%` patterns at the top-level. *)
+Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) tactic(tac) :=
+  let p :=
+    lazymatch type of p with
+    | intro_pat => eval cbv in (intro_pat_persistent p)
+    | string =>
+       let pat := intro_pat.parse_one p in
+       eval cbv in (intro_pat_persistent pat)
+    | _ => p
+    end in
+  lazymatch t with
+  | ITrm ?H ?xs ?pat =>
+    lazymatch p with
+    | true =>
+       eapply tac_specialize_persistent_helper with _ H _ _ _;
+         [env_cbv; reflexivity || fail "iSpecialize:" H "not found"
+         |iSpecializeArgs H xs; iSpecializePat H pat; last (iExact H)
+         |let Q := match goal with |- PersistentP ?Q => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
+         |env_cbv; reflexivity|tac H]
+    | false => iSpecializeArgs H xs; iSpecializePat H pat; last (tac H)
+    end
   end.
 
+Tactic Notation "iSpecialize" open_constr(t) :=
+  iSpecializeCore t as false (fun _ => idtac).
+Tactic Notation "iSpecialize" open_constr(t) "#" :=
+  iSpecializeCore t as true (fun _ => idtac).
+
 (** * Pose proof *)
 (* The tactic [iIntoEntails] tactic solves a goal [True ⊢ Q]. The arguments [t]
 is a Coq term whose type is of the following shape:
@@ -236,7 +249,7 @@ Tactic Notation "iIntoEntails" open_constr(t) :=
     end
   in go t.
 
-Tactic Notation "iPoseProofCore" open_constr(lem) "as" tactic(tac) :=
+Tactic Notation "iPoseProofCore" open_constr(lem) "as" constr(p) tactic(tac) :=
   let pose_trm t tac :=
     let Htmp := iFresh in
     lazymatch type of t with
@@ -255,16 +268,12 @@ Tactic Notation "iPoseProofCore" open_constr(lem) "as" tactic(tac) :=
     after the continuation [tac] has been called. *)
   in lazymatch lem with
   | ITrm ?t ?xs ?pat =>
-     pose_trm t ltac:(fun Htmp =>
-       iSpecializeArgs Htmp xs; iSpecializePat Htmp pat; last (tac Htmp))
+     pose_trm t ltac:(fun Htmp => iSpecializeCore (ITrm Htmp xs pat) as p tac)
   | _ => pose_trm lem tac
   end.
 
 Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
-  iPoseProofCore lem as (fun Htmp => iRename Htmp into H).
-
-Tactic Notation "iPoseProof" open_constr(lem) :=
-  iPoseProofCore lem as (fun _ => idtac).
+  iPoseProofCore lem as false (fun Htmp => iRename Htmp into H).
 
 (** * Apply *)
 Tactic Notation "iApply" open_constr(lem) :=
@@ -277,12 +286,12 @@ Tactic Notation "iApply" open_constr(lem) :=
        |lazy beta (* reduce betas created by instantiation *)]] in
   lazymatch lem with
   | ITrm ?t ?xs ?pat =>
-     iPoseProofCore t as (fun Htmp =>
+     iPoseProofCore t as false (fun Htmp =>
        iSpecializeArgs Htmp xs;
        try (iSpecializeArgs Htmp (hcons _ _));
        iSpecializePat Htmp pat; last finish Htmp)
   | _ =>
-     iPoseProofCore lem as (fun Htmp =>
+     iPoseProofCore lem as false (fun Htmp =>
        try (iSpecializeArgs Htmp (hcons _ _));
        finish Htmp)
   end.
@@ -723,7 +732,7 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
   iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ); iIntros p.
 
 (** * Destruct tactic *)
-Tactic Notation "iDestructCore" open_constr(lem) "as" tactic(tac) :=
+Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
   let intro_destruct n :=
     let rec go n' :=
       lazymatch n' with
@@ -738,49 +747,50 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" tactic(tac) :=
      let n := eval compute in (Z.to_nat lem) in intro_destruct n
   | string => tac lem
   | iTrm =>
+     (* only copy the hypothesis when universal quantifiers are instantiated *)
      lazymatch lem with
-     | @iTrm string ?H _ hnil ?pat => iSpecializePat H pat; last (tac H)
-     | _ => iPoseProofCore lem as tac
+     | @iTrm string ?H _ hnil ?pat => iSpecializeCore lem as p tac
+     | _ => iPoseProofCore lem as p tac
      end
-  | _ => iPoseProofCore lem as tac
+  | _ => iPoseProofCore lem as p tac
   end.
 
 Tactic Notation "iDestruct" open_constr(lem) "as" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
 Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
     simple_intropattern(x8) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
 Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
-  iDestructCore lem as (fun H => iPure H as pat).
+  iDestructCore lem as true (fun H => iPure H as pat).
 
 (* This is pretty ugly, but without Ltac support for manipulating lists of
 idents I do not know how to do this better. *)
@@ -823,7 +833,7 @@ Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
               ltac:(iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 )).
 
 (** * Assert *)
-Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
+Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac) :=
   let H := iFresh in
   let Hs := spec_pat.parse Hs in
   lazymatch Hs with
@@ -832,7 +842,7 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
        [env_cbv; reflexivity
        |(*goal*)
        |apply _ || fail "iAssert:" Q "not persistent"
-       |iDestructHyp H as pat]
+       |tac H]
   | [SGoal ?k ?lr ?Hs] =>
      eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
        [match k with
@@ -841,13 +851,21 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
         end
        |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
        |env_cbv; reflexivity|
-       |iDestructHyp H as pat]
+       |tac H]
   | ?pat => fail "iAssert: invalid pattern" pat
   end.
 
+Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
+  iAssertCore Q with Hs as (fun H => iDestructHyp H as pat).
 Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
   iAssert Q with "[]" as pat.
 
+Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs)
+    "as" "%" simple_intropattern(pat) :=
+  iAssertCore Q with Hs as (fun H => iPure H as pat).
+Tactic Notation "iAssert" open_constr(Q) "as" "%" simple_intropattern(pat) :=
+  iAssert Q with "[]" as %pat.
+
 (** * Rewrite *)
 Local Ltac iRewriteFindPred :=
   match goal with
@@ -857,7 +875,7 @@ Local Ltac iRewriteFindPred :=
   end.
 
 Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
-  iPoseProofCore lem as (fun Heq =>
+  iPoseProofCore lem as true (fun Heq =>
     eapply (tac_rewrite _ Heq _ _ lr);
       [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
       |let P := match goal with |- ?P ⊢ _ => P end in
@@ -869,7 +887,7 @@ Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore false lem.
 Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore true lem.
 
 Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
-  iPoseProofCore lem as (fun Heq =>
+  iPoseProofCore lem as true (fun Heq =>
     eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
       [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
       |env_cbv; reflexivity || fail "iRewrite:" H "not found"
@@ -890,45 +908,48 @@ Ltac iSimplifyEq := repeat (
 
 (** * View shifts *)
 Tactic Notation "iVs" open_constr(lem) :=
-  iDestructCore lem as (fun H => iVsCore H; last iDestruct H as "?").
+  iDestructCore lem as false (fun H => iVsCore H).
 Tactic Notation "iVs" open_constr(lem) "as" constr(pat) :=
-  iDestructCore lem as (fun H => iVsCore H; last iDestruct H as pat).
+  iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H => iVsCore H; last iDestruct H as ( x1 ) pat).
+  iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iVsCore H; last iDestruct H as ( x1 x2 ) pat).
+  iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 x2 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
-  iDestructCore lem as (fun H => iVsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
+  iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 x2 x3 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H =>
-    iVsCore H; last iDestruct H as ( x1 x2 x3 x4 ) pat).
+  iDestructCore lem as false (fun H =>
+    iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) ")" constr(pat) :=
-  iDestructCore lem as (fun H =>
-    iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 ) pat).
+  iDestructCore lem as false (fun H =>
+    iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
-  iDestructCore lem as (fun H =>
-    iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 ) pat).
+  iDestructCore lem as false (fun H =>
+    iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
     constr(pat) :=
-  iDestructCore lem as (fun H =>
-    iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+  iDestructCore lem as false (fun H =>
+    iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
 Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
     simple_intropattern(x8) ")" constr(pat) :=
-  iDestructCore lem as (fun H =>
-    iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+  iDestructCore lem as false (fun H =>
+    iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+
+Tactic Notation "iVs" open_constr(lem) "as" "%" simple_intropattern(pat) :=
+  iDestructCore lem as false (fun H => iVsCore H; iPure H as pat).
 
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
diff --git a/tests/counter.v b/tests/counter.v
index c5e84d11d76f6f8bcbcd1098e63bc885a3fa5825..8d5bb62c1b5b1fe3a1cfb6497a8d3c26de647bf9 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -113,7 +113,7 @@ Proof.
   wp_bind (CAS _ _ _). iInv N as (c') ">[Hl Hγ]" "Hclose".
   destruct (decide (c' = c)) as [->|].
   - iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (own_valid with "#Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
+    iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
     iVs (own_update with "Hγ") as "Hγ"; first apply M_update.
     rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
     wp_cas_suc. iVs ("Hclose" with "[Hl Hγ]").
@@ -129,7 +129,7 @@ Lemma read_spec l n :
 Proof.
   iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
   rewrite /read /=. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load.
-  iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[#]") as % ?%auth_frag_valid.
+  iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[-]") as % ?%auth_frag_valid.
   { iApply own_op. by iFrame. }
   rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
   iVs ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index e06e47214277a05745f7981127303fd4ba54828a..78adb9719af808df78da53ccabbe052c2db0b042 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -95,6 +95,6 @@ Proof.
     + iApply worker_spec; auto.
     + iApply worker_spec; auto.
     + auto.
-  - iIntros (_ v) "[_ H]"; iPoseProof (Q_res_join with "H"). auto.
+  - iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto.
 Qed.
 End proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 3e610b65d9ad5dd6d1549dc8575c201d0b16df37..92598f56215fafe323dfe9a0dd1e933d9f5d0aec 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -77,7 +77,7 @@ Proof.
     { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. }
     wp_load.
     iCombine "Hγ" "Hγ'" as "Hγ".
-    iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
+    iDestruct (own_valid with "Hγ") as %[=->]%dec_agree_op_inv.
     iVs ("Hclose" with "[Hl]") as "_".
     { iNext; iRight; by eauto. }
     iVsIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 49e2160cc8642d273d41f5d4b24a6293ff2db358..c6d23574cc0f589c37a9daa0329cc67094a05e2a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -68,7 +68,7 @@ Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
 Proof.
   iIntros "H1 H2".
   iRewrite (uPred.eq_sym x x with "[#]"); first done.
-  iRewrite -("H1" $! _ with "[#]"); first done.
+  iRewrite -("H1" $! _ with "[-]"); first done.
   done.
 Qed.