diff --git a/_CoqProject b/_CoqProject
index 3f01046c0098d6c83935edf7c423310d17da3f40..e5adcf5cd279a82038e8a49c99363344892ed051 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -94,6 +94,7 @@ heap_lang/lib/spawn.v
 heap_lang/lib/par.v
 heap_lang/lib/assert.v
 heap_lang/lib/lock.v
+heap_lang/lib/counter.v
 heap_lang/lib/barrier/barrier.v
 heap_lang/lib/barrier/specification.v
 heap_lang/lib/barrier/protocol.v
diff --git a/algebra/agree.v b/algebra/agree.v
index 6479419c0d202ed1d2d02664592cb5c03a5c8579..a62b288f26eaad80b7dc805c42eba32bdddfcb69 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -148,8 +148,8 @@ Arguments agreeC : clear implicits.
 Arguments agreeR : clear implicits.
 
 Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
-  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
-Solve Obligations with auto using agree_valid_S.
+  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x;
+     agree_valid_S := agree_valid_S _ x |}.
 Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
 Proof. by destruct x. Qed.
 Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
diff --git a/algebra/auth.v b/algebra/auth.v
index 45488923b38b3f830510f9639ae0707e43a2d013..4e33a44a74cbd2d3ce0863d0b95a6f98ba84e780 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -162,6 +162,9 @@ Qed.
 Canonical Structure authUR :=
   UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
 
+Global Instance auth_frag_persistent a : Persistent a → Persistent (◯ a).
+Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.
+
 (** Internalized properties *)
 Lemma auth_equivI {M} (x y : auth A) :
   x ≡ y ⊣⊢ (authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y : uPred M).
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 21e945304d7606384ab100e7cb485dae825121d6..177c51ec9f91ba22b84a3484fb0f3f00afe5f0ef 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -758,35 +758,70 @@ Section nat.
   Instance nat_validN : ValidN nat := λ n x, True.
   Instance nat_pcore : PCore nat := λ x, Some 0.
   Instance nat_op : Op nat := plus.
+  Definition nat_op_plus x y : x â‹… y = x + y := eq_refl.
   Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
   Proof.
     split.
     - intros [z ->]; unfold op, nat_op; lia.
     - exists (y - x). by apply le_plus_minus.
   Qed.
-  Lemma nat_cmra_mixin : CMRAMixin nat.
+  Lemma nat_ra_mixin : RAMixin nat.
   Proof.
-    apply discrete_cmra_mixin, ra_total_mixin; try by eauto.
+    apply ra_total_mixin; try by eauto.
     - solve_proper.
     - intros x y z. apply Nat.add_assoc.
     - intros x y. apply Nat.add_comm.
     - by exists 0.
   Qed.
-  Canonical Structure natR : cmraT :=
-    CMRAT nat (@discrete_cofe_mixin _ equivL _) nat_cmra_mixin.
+  Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
 
   Instance nat_empty : Empty nat := 0.
   Lemma nat_ucmra_mixin : UCMRAMixin nat.
   Proof. split; apply _ || done. Qed.
   Canonical Structure natUR : ucmraT :=
-    UCMRAT nat (@discrete_cofe_mixin _ equivL _) nat_cmra_mixin nat_ucmra_mixin.
+    discreteUR nat nat_ra_mixin nat_ucmra_mixin.
 
   Global Instance nat_cmra_discrete : CMRADiscrete natR.
   Proof. constructor; apply _ || done. Qed.
-  Global Instance nat_persistent (x : ()) : Persistent x.
-  Proof. by constructor. Qed.
 End nat.
 
+Definition mnat := nat.
+
+Section mnat.
+  Instance mnat_valid : Valid mnat := λ x, True.
+  Instance mnat_validN : ValidN mnat := λ n x, True.
+  Instance mnat_pcore : PCore mnat := Some.
+  Instance mnat_op : Op mnat := Nat.max.
+  Definition mnat_op_max x y : x â‹… y = x `max` y := eq_refl.
+  Lemma mnat_included (x y : mnat) : x ≼ y ↔ x ≤ y.
+  Proof.
+    split.
+    - intros [z ->]; unfold op, mnat_op; lia.
+    - exists y. by symmetry; apply Nat.max_r.
+  Qed.
+  Lemma mnat_ra_mixin : RAMixin mnat.
+  Proof.
+    apply ra_total_mixin; try by eauto.
+    - solve_proper.
+    - solve_proper.
+    - intros x y z. apply Nat.max_assoc.
+    - intros x y. apply Nat.max_comm.
+    - intros x. apply Max.max_idempotent.
+  Qed.
+  Canonical Structure mnatR : cmraT := discreteR mnat mnat_ra_mixin.
+
+  Instance mnat_empty : Empty mnat := 0.
+  Lemma mnat_ucmra_mixin : UCMRAMixin mnat.
+  Proof. split; apply _ || done. Qed.
+  Canonical Structure mnatUR : ucmraT :=
+    discreteUR mnat mnat_ra_mixin mnat_ucmra_mixin.
+
+  Global Instance mnat_cmra_discrete : CMRADiscrete mnatR.
+  Proof. constructor; apply _ || done. Qed.
+  Global Instance mnat_persistent (x : mnat) : Persistent x.
+  Proof. by constructor. Qed.
+End mnat.
+
 (** ** Product *)
 Section prod.
   Context {A B : cmraT}.
diff --git a/algebra/csum.v b/algebra/csum.v
index 5810079fd0b9d60efe345ca453a4c64fa4d61942..c4f87af3d22a83e13e5c650a445c088664a593e9 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -292,6 +292,32 @@ Proof. eauto using csum_updateP_l. Qed.
 Lemma csum_updateP'_r (P : B → Prop) b :
   b ~~>: P → Cinr b ~~>: λ m', ∃ b', m' = Cinr b' ∧ P b'.
 Proof. eauto using csum_updateP_r. Qed.
+Lemma csum_local_update_l (a1 a2 : A) af :
+  (∀ af', af = Cinl <$> af' → a1 ~l~> a2 @ af') → Cinl a1 ~l~> Cinl a2 @ af.
+Proof.
+  intros Ha. split; destruct af as [[af'| |]|]=>//=.
+  - by eapply (Ha (Some af')).
+  - by eapply (Ha None).
+  - destruct (Ha (Some af') (reflexivity _)) as [_ Ha'].
+    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
+    by apply (Ha' n (Some mz)). by apply (Ha' n None).
+  - destruct (Ha None (reflexivity _)) as [_ Ha'].
+    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
+    by apply (Ha' n (Some mz)). by apply (Ha' n None).
+Qed.
+Lemma csum_local_update_r (b1 b2 : B) bf :
+  (∀ bf', bf = Cinr <$> bf' → b1 ~l~> b2 @ bf') → Cinr b1 ~l~> Cinr b2 @ bf.
+Proof.
+  intros Hb. split; destruct bf as [[|bf'|]|]=>//=.
+  - by eapply (Hb (Some bf')).
+  - by eapply (Hb None).
+  - destruct (Hb (Some bf') (reflexivity _)) as [_ Hb'].
+    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
+    by apply (Hb' n (Some mz)). by apply (Hb' n None).
+  - destruct (Hb None (reflexivity _)) as [_ Hb'].
+    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
+    by apply (Hb' n (Some mz)). by apply (Hb' n None).
+Qed.
 End cmra.
 
 Arguments csumR : clear implicits.
diff --git a/algebra/updates.v b/algebra/updates.v
index 6b59571200f6e5a229694655593061eae30feaa3..36851cff296cf454fa3c2b37acde7c6041bcea32 100644
--- a/algebra/updates.v
+++ b/algebra/updates.v
@@ -125,6 +125,13 @@ Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1
 Proof.
   rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
 Qed.
+Lemma cmra_update_valid0 x y :
+  (✓{0} x → x ~~> y) → x ~~> y.
+Proof.
+  intros H n mz Hmz. apply H, Hmz.
+  apply (cmra_validN_le n); last lia.
+  destruct mz. eapply cmra_validN_op_l, Hmz. apply Hmz.
+Qed.
 
 (** ** Frame preserving updates for total CMRAs *)
 Section total_updates.
@@ -232,3 +239,16 @@ Section option.
   Lemma option_update x y : x ~~> y → Some x ~~> Some y.
   Proof. rewrite !cmra_update_updateP; eauto using option_updateP with subst. Qed.
 End option.
+
+(** * Natural numbers  *)
+Lemma nat_local_update (x y : nat) mz : x ~l~> y @ mz.
+Proof.
+  split; first done.
+  compute -[plus]; destruct mz as [z|]; intros n [z'|]; lia.
+Qed.
+
+Lemma mnat_local_update (x y : mnat) mz : x ≤ y → x ~l~> y @ mz.
+Proof.
+  split; first done.
+  compute -[max]; destruct mz as [z|]; intros n [z'|]; lia.
+Qed.
diff --git a/algebra/upred.v b/algebra/upred.v
index 73d521139463509343e82842df645fa8ad66e1e9..6072149717cad4add9421669ba4a36eafe5d7a47 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -564,6 +564,8 @@ Proof. intros ->; apply iff_refl. Qed.
 
 Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊢ ■ φ2.
 Proof. intros; apply pure_elim with φ1; eauto using pure_intro. Qed.
+Lemma pure_iff φ1 φ2 : (φ1 ↔ φ2) → ■ φ1 ⊣⊢ ■ φ2.
+Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
 Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
 Proof. auto. Qed.
 Lemma and_mono_l P P' Q : (P ⊢ Q) → P ∧ P' ⊢ Q ∧ P'.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
new file mode 100644
index 0000000000000000000000000000000000000000..62e3abe0a85707b296598aea94a423cc44c79762
--- /dev/null
+++ b/heap_lang/lib/counter.v
@@ -0,0 +1,84 @@
+(* Monotone counter, but using an explicit CMRA instead of auth *)
+From iris.program_logic Require Export global_functor.
+From iris.program_logic Require Import auth.
+From iris.proofmode Require Import invariants ghost_ownership coq_tactics.
+From iris.heap_lang Require Import proofmode notation.
+Import uPred.
+
+Definition newcounter : val := λ: <>, ref #0.
+Definition inc : val :=
+  rec: "inc" "l" :=
+    let: "n" := !'"l" in
+    if: CAS '"l" '"n" (#1 + '"n") then #() else '"inc" '"l".
+Definition read : val := λ: "l", !'"l".
+Global Opaque newcounter inc get.
+
+(** The CMRA we need. *)
+Class counterG Σ := CounterG { counter_tokG :> authG heap_lang Σ mnatUR }.
+Definition counterGF : gFunctorList := [authGF mnatUR].
+Instance inGF_counterG `{H : inGFs heap_lang Σ counterGF} : counterG Σ.
+Proof. destruct H; split; apply _. Qed.
+
+Section proof.
+Context {Σ : gFunctors} `{!heapG Σ, !counterG Σ}.
+Context (heapN : namespace).
+Local Notation iProp := (iPropG heap_lang Σ).
+
+Definition counter_inv (l : loc) (n : mnat) : iProp := (l ↦ #n)%I.
+
+Definition counter (l : loc) (n : nat) : iProp :=
+  (∃ N γ, heapN ⊥ N ∧ heap_ctx heapN ∧
+          auth_ctx γ N (counter_inv l) ∧ auth_own γ (n:mnat))%I.
+
+(** The main proofs. *)
+Global Instance counter_persistent l n : PersistentP (counter l n).
+Proof. apply _. Qed.
+
+Lemma newcounter_spec N (R : iProp) Φ :
+  heapN ⊥ N →
+  heap_ctx heapN ★ (∀ l, counter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}.
+Proof.
+  iIntros {?} "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
+  iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
+    as {γ} "[#? Hγ]"; try by auto.
+  iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10.
+Qed.
+
+Lemma inc_spec l j (Φ : val → iProp) :
+  counter l j ★ (counter l (S j) -★ Φ #()) ⊢ WP inc #l {{ Φ }}.
+Proof.
+  iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
+  iDestruct "Hl" as {N γ} "(% & #? & #Hγ & Hγf)".
+  wp_focus (! _)%E; iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
+  iIntros "{$Hγ $Hγf}"; iIntros {j'} "[% Hl] /="; rewrite {2}/counter_inv.
+  wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
+  wp_let; wp_op.
+  wp_focus (CAS _ _ _); iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
+  iIntros "{$Hγ $Hγf}"; iIntros {j''} "[% Hl] /="; rewrite {2}/counter_inv.
+  destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
+  - wp_cas_suc; first (by do 3 f_equal); iPvsIntro.
+    iExists (1 + j `max` j')%nat; iSplit.
+    { iPureIntro. apply mnat_local_update. abstract lia. }
+    rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia.
+    rewrite Nat2Z.inj_succ -Z.add_1_l.
+    iIntros "{$Hl} Hγf". wp_if.
+    iPvsIntro; iApply "HΦ"; iExists N, γ; repeat iSplit; eauto.
+    iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia.
+  - wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]).
+    iPvsIntro. iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
+    wp_if. iApply ("IH" with "[Hγf] HΦ"). rewrite {3}/counter; eauto 10.
+Qed.
+
+Lemma read_spec l j (Φ : val → iProp) :
+  counter l j ★ (∀ i, ■ (j ≤ i)%nat → counter l i -★ Φ #i)
+  ⊢ WP read #l {{ Φ }}.
+Proof.
+  iIntros "[Hc HΦ]". iDestruct "Hc" as {N γ} "(% & #? & #Hγ & Hγf)".
+  rewrite /read. wp_let. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
+  iIntros "{$Hγ $Hγf}"; iIntros {j'} "[% Hl] /=".
+  wp_load; iPvsIntro; iExists (j `max` j'); iSplit.
+  { iPureIntro; apply mnat_local_update; abstract lia. }
+  rewrite !mnat_op_max -Nat.max_assoc Nat.max_idempotent; iIntros "{$Hl} Hγf".
+  iApply ("HΦ" with "[%]"); first abstract lia; rewrite /counter; eauto 10.
+Qed.
+End proof.
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 8503a626fd70d265a747544e536f44e507f24076..c24b2fbd4902959fa09dff246bc3aaa325e08e2a 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -105,7 +105,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
       [let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_alloc:" e' "not a value"
       |iAssumption || fail "wp_alloc: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
         eexists; split;
@@ -126,7 +126,7 @@ Tactic Notation "wp_load" :=
       |fail 1 "wp_load: cannot find 'Load' in" e];
     eapply tac_wp_load;
       [iAssumption || fail "wp_load: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
@@ -145,7 +145,7 @@ Tactic Notation "wp_store" :=
       [let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_store:" e' "not a value"
       |iAssumption || fail "wp_store: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
@@ -167,7 +167,7 @@ Tactic Notation "wp_cas_fail" :=
       |let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_cas_fail:" e' "not a value"
       |iAssumption || fail "wp_cas_fail: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
@@ -189,7 +189,7 @@ Tactic Notation "wp_cas_suc" :=
       |let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_cas_suc:" e' "not a value"
       |iAssumption || fail "wp_cas_suc: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
diff --git a/prelude/base.v b/prelude/base.v
index fc03e031f598d2131524c7b9e6fad0a2314b1c85..c4c2eb8227a2d20700f5554db1a3a476ad273268 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -7,6 +7,7 @@ structures. *)
 Global Generalizable All Variables.
 Global Set Automatic Coercions Import.
 Global Set Asymmetric Patterns.
+Global Unset Transparent Obligations.
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
 Obligation Tactic := idtac.
 
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index e752c675b12089a3141a3f049bd7cdcccfe0665a..8fd3120cdf2d0612d7f7a39246eefda2f8e79a15 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -527,6 +527,12 @@ Proof.
   - by rewrite lookup_fmap, !lookup_insert.
   - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
 Qed.
+Lemma fmap_delete {A B} (f: A → B) m i: f <$> delete i m = delete i (f <$> m).
+Proof.
+  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
+  - by rewrite lookup_fmap, !lookup_delete.
+  - by rewrite lookup_fmap, !lookup_delete_ne, lookup_fmap by done.
+Qed.
 Lemma omap_insert {A B} (f : A → option B) m i x y :
   f x = Some y → omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
 Proof.
diff --git a/prelude/list.v b/prelude/list.v
index 42a40dc3c934e79a628aded52694c5a6ba8e6c8f..59b26331813bf82dc7cd243e88f8721e7b9fd82e 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -1265,6 +1265,21 @@ Proof.
     take_app_alt by (rewrite ?app_length, ?take_length, ?Hk; lia).
 Qed.
 
+(** ** Properties of the [imap] function *)
+Lemma imap_cons {B} (f : nat → A → B) x l :
+  imap f (x :: l) = f 0 x :: imap (f ∘ S) l.
+Proof.
+  unfold imap. simpl. f_equal. generalize 0.
+  induction l; intros n; simpl; repeat (auto||f_equal).
+Qed.
+Lemma imap_ext {B} (f g : nat → A → B) l :
+  (∀ i x, f i x = g i x) →
+  imap f l = imap g l.
+Proof.
+  unfold imap. intro EQ. generalize 0.
+  induction l; simpl; intros n; f_equal; auto.
+Qed.
+
 (** ** Properties of the [mask] function *)
 Lemma mask_nil f βs : mask f βs (@nil A) = [].
 Proof. by destruct βs. Qed.
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 50d60a0da3e354f8eda5e9190c496d5d126f15eb..0dad1337861dfe92739d36d21f2e48c4549a8aad 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -32,6 +32,8 @@ Notation "(<)" := lt (only parsing) : nat_scope.
 
 Infix "`div`" := Nat.div (at level 35) : nat_scope.
 Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
+Infix "`max`" := Nat.max (at level 35) : nat_scope.
+Infix "`min`" := Nat.min (at level 35) : nat_scope.
 
 Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
 Instance nat_le_dec: ∀ x y : nat, Decision (x ≤ y) := le_dec.
@@ -504,6 +506,8 @@ Infix "+" := Qp_plus : Qp_scope.
 Infix "-" := Qp_minus : Qp_scope.
 Infix "/" := Qp_div : Qp_scope.
 
+Instance Qp_inhabited : Inhabited Qp := populate 1%Qp.
+
 Lemma Qp_eq x y : x = y ↔ Qp_car x = Qp_car y.
 Proof.
   split; [by intros ->|].
diff --git a/prelude/strings.v b/prelude/strings.v
index 3ace24c684a4f86e7943b26625c5d6bdb0f657f3..d935c8ed6bbdcf86c09abb2d8c8f35ab81a92ec6 100644
--- a/prelude/strings.v
+++ b/prelude/strings.v
@@ -2,7 +2,12 @@
 (* This file is distributed under the terms of the BSD license. *)
 From Coq Require Import Ascii.
 From Coq Require Export String.
-From iris.prelude Require Export countable.
+From iris.prelude Require Export list.
+From iris.prelude Require Import countable.
+
+(* To avoid randomly ending up with String.length because this module is
+imported hereditarily somewhere. *)
+Notation length := List.length.
 
 (** * Fix scopes *)
 Open Scope string_scope.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 8a471ded56e799338313cb8d814cf125b727eed0..13e74464c22841fe004c0f096cc4276338d7ca91 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -412,10 +412,11 @@ Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
 It will search for the first subterm of the goal matching [pat], and then call [tac]
 with that subterm. *)
 Ltac find_pat pat tac :=
-  match goal with |- context [?x] =>
-                  unify pat x with typeclass_instances;
-                  tryif tac x then idtac else fail 2
-end.
+  match goal with
+  |- context [?x] =>
+      unify pat x with typeclass_instances;
+      tryif tac x then idtac else fail 2
+  end.
 
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
 particular, on those generated by the tactic [unfold_elem_ofs] which is used
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 6f966d983b48d95b5e2f5de6768d782fa44fa8a6..9fd82aa0723fecfe6cfa3ed40b224b8bf45669ff 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -55,6 +55,14 @@ Section auth.
 
   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.
+
+  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.
+
+  Global Instance auth_own_persistent γ a :
+    Persistent a → PersistentP (auth_own γ a).
+  Proof. rewrite /auth_own. apply _. Qed.
+
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
 
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 6b97b3d1b23963af881b54182c6c4df26185933f..0783c756414c0157085b4b592230db41bd633070 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -37,7 +37,7 @@ Section ndisjoint.
   Global Instance ndisjoint_comm : Comm iff ndisjoint.
   Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed.
 
-  Lemma ndot_ne_disjoint N (x y : A) : x ≠ y → N .@ x ⊥ N .@ y.
+  Lemma ndot_ne_disjoint N x y : x ≠ y → N .@ x ⊥ N .@ y.
   Proof. intros Hxy. exists (N .@ x), (N .@ y); naive_solver. Qed.
 
   Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → N1 .@ x ⊥ N2.
@@ -55,26 +55,17 @@ Section ndisjoint.
     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 ndisj_subseteq_difference N1 N2 E :
+    N1 ⊥ N2 → nclose N1 ⊆ E → nclose N1 ⊆ E ∖ nclose N2.
+  Proof. intros ?%ndisj_disjoint. set_solver. Qed.
 End ndisjoint.
 
-(* This tactic solves goals about inclusion and disjointness
-   of masks (i.e., coPsets) with set_solver, taking
-   disjointness of namespaces into account. *)
-(* TODO: This tactic is by far now yet as powerful as it should be.
-   For example, given [N1 ⊥ N2], it should be able to solve
-   [nclose (ndot N1 x) ⊥ N2]. It should also solve
-   [ndot N x ⊥ ndot N y] if x ≠ y is in the context or
-   follows from [discriminate]. *)
-Ltac set_solver_ndisj :=
-  repeat match goal with
-  (* TODO: Restrict these to have type namespace *)
-  | [ H : ?N1 ⊥ ?N2 |-_ ] => apply ndisj_disjoint in H
-  end; set_solver.
-(* TODO: restrict this to match only if this is ⊆ of coPset *)
-Hint Extern 500 (_ ⊆ _) => set_solver_ndisj : ndisj.
 (* The hope is that registering these will suffice to solve most goals
-   of the form [N1 ⊥ N2].
-   TODO: Can this prove x ≠ y if discriminate can? *)
-Hint Resolve ndot_ne_disjoint : ndisj.
+of the form [N1 ⊥ N2] and those of the form [((N1 ⊆ E ∖ N2) ∖ ..) ∖ Nn]. *)
+Hint Resolve ndisj_subseteq_difference : ndisj.
+Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj.
 Hint Resolve ndot_preserve_disjoint_l : ndisj.
 Hint Resolve ndot_preserve_disjoint_r : ndisj.
+
+Ltac solve_ndisj := solve [eauto with ndisj].
diff --git a/proofmode/classes.v b/proofmode/classes.v
index b30f4311c5ca4cc0840a05f2bbad5867ffef12a5..b8d444380cc0e820727c3090cb7c5344bf3c6388 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -112,10 +112,10 @@ Global Arguments from_and : clear implicits.
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
 Proof. done. Qed.
 Global Instance from_and_sep_persistent_l P1 P2 :
-  PersistentP P1 → FromAnd (P1 ★ P2) P1 P2.
+  PersistentP P1 → FromAnd (P1 ★ P2) P1 P2 | 9.
 Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
 Global Instance from_and_sep_persistent_r P1 P2 :
-  PersistentP P2 → FromAnd (P1 ★ P2) P1 P2.
+  PersistentP P2 → FromAnd (P1 ★ P2) P1 P2 | 10.
 Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
 Global Instance from_and_always P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index 6595977c93d8767e440f14281550a01f2e9f526e..0f55cbf3b034bf6bb7f220ec16f66318c4c2db33 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -13,7 +13,7 @@ Inductive intro_pat :=
   | INext : intro_pat
   | IForall : intro_pat
   | IAll : intro_pat
-  | IClear : list string → intro_pat.
+  | IClear : list (bool * string) → intro_pat. (* true = frame, false = clear *)
 
 Module intro_pat.
 Inductive token :=
@@ -71,8 +71,7 @@ Inductive stack_item :=
   | SList : stack_item
   | SConjList : stack_item
   | SBar : stack_item
-  | SAmp : stack_item
-  | SClear : stack_item.
+  | SAmp : stack_item.
 Notation stack := (list stack_item).
 
 Fixpoint close_list (k : stack)
@@ -108,13 +107,6 @@ Fixpoint close_conj_list (k : stack)
   | _ => None
   end.
 
-Fixpoint close_clear (k : stack) (ss : list string) : option stack :=
-  match k with
-  | SPat (IName s) :: k => close_clear k (s :: ss)
-  | SClear :: k => Some (SPat (IClear (reverse ss)) :: k)
-  | _ => None
-  end.
-
 Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   match ts with
   | [] => Some k
@@ -135,9 +127,18 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TNext :: ts => parse_go ts (SPat INext :: k)
   | TAll :: ts => parse_go ts (SPat IAll :: k)
   | TForall :: ts => parse_go ts (SPat IForall :: k)
-  | TClearL :: ts => parse_go ts (SClear :: k)
-  | TClearR :: ts => close_clear k [] ≫= parse_go ts
+  | TClearL :: ts => parse_clear ts [] k
+  | _ => None
+  end
+with parse_clear (ts : list token)
+    (ss : list (bool * string)) (k : stack) : option stack :=
+  match ts with
+  | TFrame :: TName s :: ts => parse_clear ts ((true,s) :: ss) k
+  | TName s :: ts => parse_clear ts ((false,s) :: ss) k
+  | TClearR :: ts => parse_go ts (SPat (IClear (reverse ss)) :: k)
+  | _ => None
   end.
+
 Definition parse (s : string) : option (list intro_pat) :=
   match k ← parse_go (tokenize s) [SList]; close_list k [] [] with
   | Some [SPat (IList [ps])] => Some ps
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index 48277e7cf32e364d58b8e12a9c6656f7a9c6ccca..bb080ac1b7dfabed64fb08234b206e2a2983c0ff 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -39,7 +39,7 @@ Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
     [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
     |try fast_done (* atomic *)
-    |done || eauto with ndisj (* [eauto with ndisj] is slow *)
+    |solve_ndisj
     |iAssumption || fail "iInv: invariant" N "not found"
     |env_cbv; reflexivity
     |simpl (* get rid of FSAs *)].
@@ -65,7 +65,7 @@ Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
     [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
     |try fast_done (* atomic *)
-    |done || eauto with ndisj (* [eauto with ndisj] is slow *)
+    |solve_ndisj
     |iAssumption || fail "iOpenInv: invariant" N "not found"
     |let P := match goal with |- TimelessP ?P => P end in
      apply _ || fail "iInv:" P "not timeless"
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index 4ef97c10b67a210d2ab7c6787ac36b69d22a3d82..6489692eae596672c8a5e3ee1d2e0b99c171c8c6 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -42,32 +42,29 @@ Inductive state :=
   | StTop : state
   | StAssert : spec_goal_kind → bool → list string → state.
 
-Fixpoint parse_go (ts : list token) (s : state)
-    (k : list spec_pat) : option (list spec_pat) :=
-  match s with
-  | StTop =>
-     match ts with
-     | [] => Some (rev k)
-     | TName s :: ts => parse_go ts StTop (SName false s :: k)
-     | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts StTop (SGoalPersistent :: k)
-     | TBracketL :: TPure :: TBracketR :: ts => parse_go ts StTop (SGoalPure :: k)
-     | TBracketL :: ts => parse_go ts (StAssert GoalStd false []) k
-     | TPvs :: TBracketL :: ts => parse_go ts (StAssert GoalPvs false []) k
-     | TPvs :: ts => parse_go ts StTop (SGoal GoalPvs true [] :: k)
-     | TPersistent :: TName s :: ts => parse_go ts StTop (SName true s :: k)
-     | TForall :: ts => parse_go ts StTop (SForall :: k)
-     | _ => None
-     end
-  | StAssert kind neg ss =>
-     match ts with
-     | TMinus :: ts => guard (¬neg ∧ ss = []); parse_go ts (StAssert kind true ss) k
-     | TName s :: ts => parse_go ts (StAssert kind neg (s :: ss)) k
-     | TBracketR :: ts => parse_go ts StTop (SGoal kind neg (rev ss) :: k)
-     | _ => None
-     end
+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)
+  | 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
+  | TPvs :: TBracketL :: ts => parse_goal ts GoalPvs false [] k
+  | TPvs :: ts => parse_go ts (SGoal GoalPvs true [] :: k)
+  | TPersistent :: TName s :: ts => parse_go ts (SName true s :: k)
+  | TForall :: ts => parse_go ts (SForall :: k)
+  | _ => None
+  end
+with parse_goal (ts : list token) (kind : spec_goal_kind)
+    (neg : bool) (ss : list string) (k : list spec_pat) : option (list spec_pat) :=
+  match ts with
+  | TMinus :: ts => guard (¬neg ∧ ss = []); parse_goal ts kind true ss k
+  | TName s :: ts => parse_goal ts kind neg (s :: ss) k
+  | TBracketR :: ts => parse_go ts (SGoal kind neg (reverse ss) :: k)
+  | _ => None
   end.
 Definition parse (s : string) : option (list spec_pat) :=
-  parse_go (tokenize s) StTop [].
+  parse_go (tokenize s) [].
 
 Ltac parse s :=
   lazymatch type of s with
diff --git a/proofmode/sts.v b/proofmode/sts.v
index 4b535fb3c5dc74ee37b52b283fd1f326212ae8f9..c0c469b06ba1e2251d26347b869477b95de2aa37 100644
--- a/proofmode/sts.v
+++ b/proofmode/sts.v
@@ -41,6 +41,6 @@ Tactic Notation "iSts" constr(H) "as"
     |try fast_done (* atomic *)
     |iAssumptionCore || fail "iSts:" H "not found"
     |iAssumption || fail "iSts: invariant not found"
-    |done || eauto with ndisj (* [eauto with ndisj] is slow *)
+    |solve_ndisj
     |intros s Hs; eexists; split; [env_cbv; reflexivity|simpl]].
 Tactic Notation "iSts" constr(H) "as" simple_intropattern(s) := iSts H as s ?.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index a3de35f17cfe8afb1edcab027762cab910c29cd1..63e04aed97486700d750fa3dc2233740f2d4083e 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -560,7 +560,13 @@ Tactic Notation "iIntros" constr(pat) :=
     | ISimpl :: ?pats => simpl; go pats
     | IAlways :: ?pats => iAlways; go pats
     | INext :: ?pats => iNext; go pats
-    | IClear ?Hs :: ?pats => iClear Hs; go pats
+    | IClear ?cpats :: ?pats =>
+       let rec clr cpats :=
+         match cpats with
+         | [] => go pats
+         | (false,?H) :: ?cpats => iClear H; clr cpats
+         | (true,?H) :: ?cpats => iFrame H; clr cpats
+         end in clr cpats
     | IPersistent (IName ?H) :: ?pats => iIntro #H; go pats
     | IName ?H :: ?pats => iIntro H; go pats
     | IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 768662ea387d2fb1cfdefd31c4ee3ec49d0f5254..6cd42173339fe1af53a0820c71a1f977046a8307 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -52,11 +52,11 @@ Proof.
   iPvsIntro. iApply "Hf"; iSplit.
   - iIntros {n} "!". wp_let.
     iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
-    + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft].
+    + wp_cas_suc. iSplitL; [|by iLeft].
       iPvs (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Cinr (DecAgree n)). }
       iPvsIntro; iRight; iExists n; by iSplitL "Hl".
-    + wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight.
+    + wp_cas_fail. rewrite /one_shot_inv; eauto 10.
   - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
     iAssert (∃ v, l ↦ v ★ ((v = InjLV #0 ★ own γ Pending) ∨
        ∃ n : Z, v = InjRV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "Hv".
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 67eee7e4d9fe07540ddda92db0b872aa46ffca9d..e0694d4b26e8e66002bf0d64507ec29cb56d47c7 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -28,7 +28,7 @@ Proof.
   iRevert {a b} "Ha Hb". iIntros {b a} "Hb {foo} Ha".
   iAssert (uPred_ownM (a â‹… core a)) with "[Ha]" as "[Ha #Hac]".
   { by rewrite cmra_core_r. }
-  iFrame "Ha Hac".
+  iIntros "{$Hac $Ha}".
   iExists (S j + z1), z2.
   iNext.
   iApply ("H3" $! _ 0 with "H1 []").