diff --git a/opam b/opam
index fc65817563313192dc793809e1f713b17a8fd8f4..ff8097f2bdea98c59a13a968c46b01a43433c72d 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2019-05-09.1.d0daa181") | (= "dev") }
+  "coq-iris" { (= "dev.2019-05-15.0.551c1ecc") | (= "dev") }
 ]
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 05315b8ca366ec038cd967817a2f899ded151084..7418153b929720ea1ad06abf85a2df36eec83a3e 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -24,7 +24,8 @@ Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
   iMod (own_alloc (● to_heap σ)) as (vγ) "Hvγ".
   { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
-  iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ"; first done.
+  iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ";
+    first by apply auth_auth_valid.
   set (Hheap := HeapG _ _ _ vγ fγ).
   iModIntro. iExists (λ σ _, heap_ctx σ). iSplitL.
   { iExists ∅. by iFrame. }
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 2c3acda7993eef04768f3705dfa9c426fd164a53..93a6f98ba47ac61f3bde17420c263dca56336748 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -142,7 +142,7 @@ Section heap.
   Lemma heap_mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
   Proof.
     rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
-    eapply pure_elim; [done|]=> /auth_own_valid /=.
+    eapply pure_elim; [done|]=> /auth_frag_valid /=.
     rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
   Qed.
 
@@ -215,7 +215,7 @@ Section heap.
       {[l +â‚— i := (q, Cinr 0%nat, to_agree v)]}).
   Proof.
     rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
-    by rewrite (big_opL_commute (Auth None)) big_opL_commute1 //.
+    by rewrite /auth_frag (big_opL_commute (Auth None)) big_opL_commute1 //.
   Qed.
 
   Global Instance heap_mapsto_pred_fractional l (P : list val → iProp Σ):
@@ -406,7 +406,7 @@ Section heap.
   Proof.
     iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
     iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
-    iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid.
     move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
     apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
     { move: (Hv (l.1)). rewrite Hl. by intros [??]. }
@@ -429,7 +429,7 @@ Section heap.
         σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
   Proof.
     iIntros "H● H◯".
-    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
     iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
     rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
@@ -446,7 +446,7 @@ Section heap.
     ⌜σ !! l = Some (ls, v)⌝.
   Proof.
     iIntros "H● H◯".
-    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
     iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
     rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index b63b63ce7593da6acc0b308253a44c8fbd2569e6..a9c1c933e814776b459f3760af4bc56c532fe076 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -189,7 +189,7 @@ Section arc.
     iIntros "Hl1 Hl2 [HP1 HP1']".
     iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH, None), O) ⋅
                       â—¯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
-      as (γ) "[H● H◯]"; first done.
+      as (γ) "[H● H◯]"; first by apply auth_both_valid.
     iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
     rewrite Qp_div_2. auto.
   Qed.
@@ -198,7 +198,8 @@ Section arc.
     l ↦ #0 -∗ (l +ₗ 1) ↦ #1 -∗ P2 ={E}=∗ ∃ γ, is_arc P1 P2 N γ l ∗ weak_tok γ.
   Proof.
     iIntros "Hl1 Hl2 HP2".
-    iMod (own_alloc ((● (None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H● H◯]"; first done.
+    iMod (own_alloc ((● (None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H● H◯]";
+      first by apply auth_both_valid.
     iExists _. iFrame. iApply inv_alloc. iExists _. iFrame.
   Qed.
 
@@ -209,7 +210,7 @@ Section arc.
                              else ∃ q'', q' = (q + q'')%Qp⌝.
   Proof.
     iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
-        %[[Hincl%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
+        %[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid.
     destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
       simpl in *; subst.
     - setoid_subst. iExists _, _, _, _. by iSplit.
@@ -336,7 +337,7 @@ Section arc.
   Proof.
     iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
         %[[Hincl%option_included Hincl'%nat_included]%prod_included [Hval _]]
-         %auth_valid_discrete_2.
+         %auth_both_valid.
     destruct st as [?[]], Hincl as [_|(?&?&[=]&?)]; simpl in *; try lia. eauto.
   Qed.
 
@@ -491,7 +492,7 @@ Section arc.
   Proof.
     iIntros "INV H◯ HP2". iInv N as ([st ?]) "[>H● H]" "Hclose".
     iDestruct (own_valid_2 with "H● H◯")
-      as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
+      as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
     simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
         try done; try apply _. setoid_subst.
     iMod (own_update_2 with "H● H◯") as "[H● $]".
@@ -588,7 +589,7 @@ Section arc.
       iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame.
       iModIntro. wp_case. wp_bind (!ˢᶜ_)%E. iInv N as ([st ?]) "[>H● H]" "Hclose".
       iDestruct (own_valid_2 with "H● H◯") as
-        %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
+        %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
       simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
       + apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
         destruct Hincl as (?&[[??]?]&[=<-]&->&[[_ Hlt]%prod_included _]%prod_included).
@@ -598,7 +599,7 @@ Section arc.
         iModIntro. wp_let. wp_op; case_bool_decide; [lia|]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
         iInv N as ([st w]) "[>H● H]" "Hclose".
         iDestruct (own_valid_2 with "H● H◯") as
-           %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
+           %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid.
         simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first.
         assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
         { destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
@@ -650,7 +651,7 @@ Section arc.
       clear w. iModIntro. wp_case. wp_op. wp_bind (!ˢᶜ_)%E.
       iInv N as ([st w']) "[>H● H]" "Hclose".
       iDestruct (own_valid_2 with "H● H◯")
-        as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
+        as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
       simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
         [|by apply _|done]. setoid_subst. iDestruct "H" as "[Hl Hl1]".
       wp_read. destruct w'.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 573c445693d8dc84273e5695db86b3bb9c4706bd..bd164ce8861247fa491240bf05a456d5f9d2696a 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -19,7 +19,7 @@ Proof.
   iIntros (?) "Hslice Halive Hbor Htok". unfold lft_bor_alive, idx_bor_own.
   iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
   iDestruct (own_bor_valid_2 with "Hown Hbor")
-    as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+    as %[EQB%to_borUR_included _]%auth_both_valid.
   iMod (slice_empty _ _ true with "Hslice Hbox") as "[$ Hbox]".
     solve_ndisj. by rewrite lookup_fmap EQB.
   rewrite -(fmap_insert bor_filled _ _ (Bor_open q)).
@@ -41,7 +41,7 @@ Proof.
   iIntros (?) "Hslice Halive Hbor HP". unfold lft_bor_alive, idx_bor_own.
   iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
   iDestruct (own_bor_valid_2 with "Hown Hbor")
-    as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+    as %[EQB%to_borUR_included _]%auth_both_valid.
   iMod (slice_fill _ _ true with "Hslice HP Hbox") as "Hbox".
     solve_ndisj. by rewrite lookup_fmap EQB.
   rewrite -(fmap_insert bor_filled _ _ Bor_in).
@@ -100,7 +100,7 @@ Proof.
       iLeft. iFrame "%". iExists _, _. iFrame.
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hf")
-        as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
+        as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_both_valid.
       by destruct INCL as [[=]|(? & ? & [=<-] &
         [[_<-]%lookup_gset_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
   - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
@@ -124,7 +124,7 @@ Proof.
     unfold lft_bor_alive.
     iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
     iDestruct (own_bor_valid_2 with "Hown Hbor")
-      as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+      as %[EQB%to_borUR_included _]%auth_both_valid.
     iMod (slice_empty _ _ true with "Hs Hbox") as "[HP' Hbox]".
       solve_ndisj. by rewrite lookup_fmap EQB.
     iDestruct ("HPP'" with "HP'") as "$".
@@ -176,7 +176,7 @@ Proof.
       iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
       iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
       iDestruct (own_bor_valid_2 with "Hown Hbor")
-        as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+        as %[EQB%to_borUR_included _]%auth_both_valid.
       iMod (slice_delete_empty _ _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
         solve_ndisj. by rewrite lookup_fmap EQB.
       iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
@@ -204,7 +204,7 @@ Proof.
       iExists Q. rewrite -bi.iff_refl. eauto.
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hbor")
-        as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
+        as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_both_valid.
       by destruct INCL as [[=]|(? & ? & [=<-] &
         [[_<-]%lookup_gset_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
   - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
@@ -231,7 +231,7 @@ Proof.
     unfold lft_bor_alive, idx_bor_own.
     iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
     iDestruct (own_bor_valid_2 with "Hown Hbor")
-      as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+      as %[EQB%to_borUR_included _]%auth_both_valid.
     iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
       solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
     iMod fupd_intro_mask' as "Hclose"; last iIntros "!>* HvsQ HQ". solve_ndisj.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 70b98634a788feb1d7719f59e7d6c81dedc55aef..aa0c17632e6bd3a9cb23e03efdc6698412548454 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -25,7 +25,7 @@ Proof.
     iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
     iDestruct "H" as (B) "(Hbox & >Hown & HB)".
     iDestruct (own_bor_valid_2 with "Hown Hbor")
-        as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+        as %[EQB%to_borUR_included _]%auth_both_valid.
     iMod (slice_iff _ _ true with "HPP' Hslice Hbox")
       as (s' Pb') "(% & #HPbPb' & Hslice & Hbox)"; first solve_ndisj.
     { by rewrite lookup_fmap EQB. }
@@ -93,9 +93,9 @@ Proof.
     iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
     iDestruct "H" as (B) "(Hbox & >Hown & HB)".
     iDestruct (own_bor_valid_2 with "Hown Hbor1")
-        as %[EQB1%to_borUR_included _]%auth_valid_discrete_2.
+        as %[EQB1%to_borUR_included _]%auth_both_valid.
     iDestruct (own_bor_valid_2 with "Hown Hbor2")
-        as %[EQB2%to_borUR_included _]%auth_valid_discrete_2.
+        as %[EQB2%to_borUR_included _]%auth_both_valid.
     iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
     { iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
       iPureIntro. iIntros (->). (* FIXME this used to work without iPureIntro. *)
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 672bf284e96dd6f8a73123c3d6487267ac4eaed0..72ed90493ad28c5bf259811b68e8b3cfdbf9d4db 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -32,7 +32,7 @@ Proof.
     iDestruct (@big_sepS_elem_of with "Hdead") as "Hdead"; first by eauto.
     rewrite /lft_inv_dead; iDestruct "Hdead" as (R) "(_ & Hcnt' & _)".
     iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
-      as %[?%nat_included _]%auth_valid_discrete_2; lia. }
+      as %[?%nat_included _]%auth_both_valid; lia. }
   iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver.
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
@@ -129,7 +129,7 @@ Proof.
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   rewrite /lft_tok big_sepMS_singleton.
   iDestruct (own_valid_2 with "HA HΛ")
-    as %[[s [?%leibniz_equiv ?]]%singleton_included _]%auth_valid_discrete_2.
+    as %[[s [?%leibniz_equiv ?]]%singleton_included _]%auth_both_valid.
   iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
   { by eapply auth_update, singleton_local_update,
       (exclusive_local_update _ (Cinr ())). }
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index decf7ad3365dc6db755aa6cf0fb5913dd350a51e..58c3ebe5a07fb7184027a1a11f8be57fa0bf9b46 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -16,12 +16,12 @@ Proof.
   iIntros "HA HI Hinv".
   destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
   { iModIntro. iExists A, I. by iFrame. }
-  iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first done.
+  iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid.
   iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
       (frac * agree bor_stateC)))) as (γbor) "[Hbor Hbor']";
-    first by apply auth_valid_discrete_2.
+    first by apply auth_both_valid.
   iMod (own_alloc ((● ε) :auth (gset_disj slice_name)))
-     as (γinh) "Hinh"; first by done.
+     as (γinh) "Hinh"; first by apply auth_auth_valid.
   set (γs := LftNames γbor γcnt γinh).
   iMod (own_update with "HI") as "[HI Hγs]".
   { apply auth_update_alloc,
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 4086a8242518b082a6fe2a6fb9f3d4cb006b1f62..6d16148d07d1f843c3bb8fe0af54602572c2cb0b 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -22,8 +22,8 @@ Lemma lft_init `{!lftPreG Σ} E :
   ↑lftN ⊆ E → (|={E}=> ∃ _ : lftG Σ, lft_ctx)%I.
 Proof.
   iIntros (?). rewrite /lft_ctx.
-  iMod (own_alloc (● ∅ : authR alftUR)) as (γa) "Ha"; first done.
-  iMod (own_alloc (● ∅ : authR ilftUR)) as (γi) "Hi"; first done.
+  iMod (own_alloc (● ∅ : authR alftUR)) as (γa) "Ha"; first by apply auth_auth_valid.
+  iMod (own_alloc (● ∅ : authR ilftUR)) as (γi) "Hi"; first by apply auth_auth_valid.
   set (HlftG := LftG _ _ _ γa _ γi _ _ _). iExists HlftG.
   iMod (inv_alloc _ _ lfts_inv with "[Ha Hi]") as "$"; last done.
   iModIntro. rewrite /lfts_inv /own_alft_auth /own_ilft_auth. iExists ∅, ∅.
@@ -37,7 +37,7 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
     own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
-    as %[[? [Hl ?]]%singleton_included _]%auth_valid_discrete_2.
+    as %[[? [Hl ?]]%singleton_included _]%auth_both_valid.
   unfold to_ilftUR in *. simplify_map_eq.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.
@@ -47,7 +47,7 @@ Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
     own alft_name (◯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some b⌝.
 Proof.
   iIntros "HA HΛ".
-  iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_valid_discrete_2.
+  iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid.
   iPureIntro. move: HA=> /singleton_included [qs [/leibniz_equiv_iff]].
   rewrite lookup_fmap fmap_Some=> -[b' [? ->]] /Some_included.
   move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
@@ -65,8 +65,8 @@ Proof.
   { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
-  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL' <-.
+  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
+  rewrite -auth_frag_op auth_frag_valid op_singleton singleton_valid=> /agree_op_invL' <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_op κ x x1 x2 :
@@ -99,14 +99,14 @@ Proof.
   { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
-  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL'=> <-.
+  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
+  rewrite -auth_frag_op auth_frag_valid op_singleton singleton_valid=> /agree_op_invL'=> <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_cnt_into_op κ x x1 x2 :
   IsOp x x1 x2 → IntoSep (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
 Proof.
-  rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_cnt_op.
+  rewrite /IsOp /IntoSep=> ->. by rewrite -own_cnt_op.
 Qed.
 Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
@@ -133,14 +133,14 @@ Proof.
   { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
-  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL' <-.
+  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
+  rewrite -auth_frag_op auth_frag_valid op_singleton singleton_valid=> /agree_op_invL'=> <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_inh_into_op κ x x1 x2 :
   IsOp x x1 x2 → IntoSep (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
 Proof.
-  rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_inh_op.
+  rewrite /IsOp /IntoSep=> ->. by rewrite -own_inh_op.
 Qed.
 Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
@@ -277,7 +277,7 @@ Proof.
   rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
   iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //.
   iDestruct (own_valid_2 with "H H'") as %Hvalid.
-  move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
+  move: Hvalid=> /auth_frag_valid /=; by rewrite op_singleton singleton_valid.
 Qed.
 
 Lemma lft_tok_static q : q.[static]%I.
@@ -452,12 +452,12 @@ Proof.
   iModIntro. iSplitL "Hbox HE".
   { iNext. rewrite /lft_inh. iExists ({[γE]} ∪ PE).
     rewrite gset_to_gmap_union_singleton. iFrame. }
-  clear dependent PE. rewrite -(left_id_L ε op (◯ GSet {[γE]})).
+  clear dependent PE. rewrite -(left_id ε op (◯ GSet {[γE]})).
   iDestruct "HEâ—¯" as "[HEâ—¯' HEâ—¯]". iSplitL "HEâ—¯'".
   { iIntros (I) "HI". iApply (own_inh_auth with "HI HEâ—¯'"). }
   iIntros (Q'). rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
   iDestruct (own_inh_valid_2 with "HE HEâ—¯")
-    as %[Hle%gset_disj_included _]%auth_valid_discrete_2.
+    as %[Hle%gset_disj_included _]%auth_both_valid.
   iMod (own_inh_update_2 with "HE HEâ—¯") as "HE".
   { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
   iMod (slice_delete_full _ _ true with "Hslice Hbox")
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index d7e2e4b09e6450515dbfa576c126f06b218dae41..283317ab260b58152abda4b70494606ce3e14353 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -34,7 +34,7 @@ Proof.
     iDestruct "Hκ" as (Pb' Pi') "(Hκalive&Hvs'&Hinh')".
   rewrite {2}/lft_bor_alive; iDestruct "Hκalive" as (B) "(Hbox & >HB● & HB)".
   iDestruct (own_bor_valid_2 with "HB● Hi")
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
+    as %[HB%to_borUR_included _]%auth_both_valid.
   iMod (slice_empty _ _ true with "Hislice Hbox") as "[HP Hbox]"; first done.
   { by rewrite lookup_fmap HB. }
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
@@ -75,7 +75,7 @@ Proof.
   iDestruct ("Hκalive" with "[//]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)".
   rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
   iDestruct (own_bor_valid_2 with "HB● Hi")
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
+    as %[HB%to_borUR_included _]%auth_both_valid.
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
   { eapply auth_update, singleton_local_update,
      (exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
@@ -118,7 +118,7 @@ Proof.
   iDestruct "Hinvκ" as (Pb Pi) "(Halive & Hvs & Hinh)".
   iDestruct "Halive" as (B) "(Hbox & >H● & HB)".
   iDestruct (own_bor_valid_2 with "H● Hbor")
-    as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+    as %[EQB%to_borUR_included _]%auth_both_valid.
   iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
     solve_ndisj. by rewrite lookup_fmap EQB.
   iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 742eea032c52e3ac65e1d84b2c696706294059d8..d74d620b91d9be9806ef14a9c5054c5912816098 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree excl.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
@@ -159,7 +159,7 @@ Section rc.
         iMod (bor_create with "LFT Hown") as "[HP HPend]"; first solve_ndisj.
         iMod (own_alloc (● (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat) ⋅
                          ◯ (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat))) as (γ) "[Ha Hf]".
-        { by apply auth_valid_discrete_2. }
+        { by apply auth_both_valid. }
         iMod (na_inv_alloc tid _ _ (rc_inv tid ν γ l' ty)
               with "[Ha Hν2 Hl'1 Hl'2 H† HPend]") as "#?".
         { rewrite /rc_inv. iExists (Some $ Cinl (_, _), _). iFrame. iExists _.
@@ -282,7 +282,7 @@ Section code.
       iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
       iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
       iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
-        %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
+        %option_included _]%prod_included [Hval _]]%auth_both_valid.
       simpl in EQst'. subst st. destruct Hincl as [Hincl|Hincl].
       + destruct st' as [[]| |]; try by inversion Hincl. apply (inj Cinl) in Hincl.
         apply (inj2 pair) in Hincl. destruct Hincl as [<-%leibniz_equiv <-%leibniz_equiv].
@@ -337,7 +337,7 @@ Section code.
           iMod (na_inv_open with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
           iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
           iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
-            %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
+            %option_included _]%prod_included [Hval _]]%auth_both_valid.
           simpl in EQst'. subst st. destruct Hincl as [Hincl|Hincl]; first last.
           { apply csum_included in Hincl. destruct Hincl as
              [->|[(?&?&[=]&?)|(?&?&[=<-]&->&?%exclusive_included)]]; try done. apply _. }
@@ -408,7 +408,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
-               %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
       apply csum_included in Hincl. naive_solver. }
@@ -467,7 +467,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
-               %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
       apply csum_included in Hincl. naive_solver. }
@@ -572,7 +572,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
-               %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
       apply csum_included in Hincl. naive_solver. }
@@ -1066,7 +1066,8 @@ Section code.
         with "[>Hty]" as (γ ν q') "(Hty & Htok & Hν)".
       { iDestruct "Hty" as "[(Hl1 & Hl2 & Hl† & Hl3)|Hty]"; last done.
         iMod (own_alloc (● (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat) ⋅
-                         rc_tok (1/2)%Qp)) as (γ) "[Ha Hf]"=>//.
+                         rc_tok (1/2)%Qp)) as (γ) "[Ha Hf]";
+          first by apply auth_both_valid.
         iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] #Hν†]"=>//.
         iApply (fupd_mask_mono (↑lftN))=>//. iExists γ, ν, (1/2)%Qp. iFrame.
         iMod (bor_create _ ν with "LFT Hl3") as "[Hb Hh]"=>//. iExists _.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 12ab5f8b4e3eb63a2bdb423959fa34ce3f0b957f..230bbf11468dad4103d96e6bb7255f49d1abf50b 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -158,7 +158,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hwtok") as
-      %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_valid_discrete_2.
+      %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
     destruct st as [[[q'' strong]| |]|]; try done.
     - (* Success case. *)
       iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >Hq''q0 & [Hν1 Hν2] & Hν†)".
@@ -261,7 +261,7 @@ Section code.
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
     iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
-               %option_included _]%prod_included [Hval _]]%auth_valid_discrete_2;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
       apply csum_included in Hincl. naive_solver. }
@@ -327,7 +327,7 @@ Section code.
       iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
       iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
       iDestruct (own_valid_2 with "Hrc● Hwtok") as
-        %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_valid_discrete_2.
+        %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
       iMod (own_update with "Hrc●") as "[Hrc● $]".
       { by apply auth_update_alloc, prod_local_update_2,
            (op_local_update_discrete _ _ 1%nat). }
@@ -400,7 +400,7 @@ Section code.
       iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose)"; [solve_ndisj..|].
       iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
       iDestruct (own_valid_2 with "Hrc● Hwtok") as
-          %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_valid_discrete_2.
+          %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
       destruct weakc; first by simpl in *; lia.
       iMod (own_update_2 with "Hrc● Hwtok") as "Hrc●".
       { apply auth_update_dealloc, prod_local_update_2,
@@ -473,7 +473,7 @@ Section code.
     { rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
       iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
       iMod (own_alloc (● _ ⋅ ◯ _)) as (γ) "[??]"; last (iExists _, _; iFrame).
-      { apply auth_valid_discrete_2. by split. }
+      { apply auth_both_valid. by split. }
       iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
       iSplitL; last by iRight. iMod (na_inv_alloc with "[-]") as "$"; last done.
       iExists _. iFrame. rewrite freeable_sz_full_S shift_loc_assoc. iFrame.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 181d9dde4231d48afd1569f28c9b36b9fb75132f..35d2901d534d21887080156fe22e67f386b7adb9 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -26,7 +26,7 @@ Section ref_functions.
     { destruct st as [[[[??]?]?]|];
       iDestruct (own_valid_2 with "H● H◯")
         as %[[[=]|(?&[[? q'] n]&[=<-]&[=]&[[[Eq_ag ?%leibniz_equiv]_]|Hle])]
-               %option_included Hv]%auth_valid_discrete_2; simpl in *; subst.
+               %option_included Hv]%auth_both_valid; simpl in *; subst.
       - apply (inj to_agree), (inj2 pair) in Eq_ag.
         destruct Eq_ag. setoid_subst. eauto.
       - revert Hle=> /prod_included [/= /prod_included
@@ -166,7 +166,7 @@ Section ref_functions.
       with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
     { iDestruct (own_valid with "H●◯") as
           %[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included]
-              %Some_included _]%auth_valid_discrete_2.
+              %Some_included _]%auth_both_valid.
       - simpl in *. setoid_subst.
         iExists None. iFrame. iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index ebb22ebaa14bd2a1725246884ba2e7dfca9a4858..b82faca971fd972523650f9c5c9a5bc669ba535c 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -137,7 +137,8 @@ Section refcell.
       - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
         iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
     clear dependent n. iDestruct "H" as ([|n|n]) "Hn"; try lia.
-    - iFrame. iMod (own_alloc (● None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
+    - iFrame. iMod (own_alloc (● None)) as (γ) "Hst"; first by apply auth_auth_valid.
+      iExists γ, None. by iFrame.
     - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
       iMod (own_alloc (● (refcell_st_to_R $ Some (ν, false, (1/2)%Qp, n)))) as (γ) "Hst".
       { by apply auth_auth_valid. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 719970bd442560d8103510fca3b35726a69e5c19..43e251302e8a45789ff301d142f5b703b117102f 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -131,7 +131,7 @@ Section refmut_functions.
       with "[H↦lrc H● H◯ Hν INV]" as "INV".
     { iDestruct (own_valid_2 with "H● H◯") as
         %[[[=]|(? & [[? q'] ?] & [= <-] & Hst & INCL)]%option_included _]
-         %auth_valid_discrete_2.
+         %auth_both_valid.
       destruct st as [[[[??]?]?]|]; [|done]. move: Hst=>-[= ???]. subst.
       destruct INCL as [[[[ν' ?]%to_agree_inj ?] ?]|
             [[[??]%to_agree_included [q'' Hq'']]%prod_included [n' Hn']]%prod_included].
@@ -299,7 +299,7 @@ Section refmut_functions.
     iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
     wp_seq. wp_op. wp_read.
     iDestruct "INV" as (st) "(Hlrc & H● & Hst)".
-    iDestruct (own_valid_2 with "H● Hγ") as %[Hst _]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "H● Hγ") as %[Hst _]%auth_both_valid.
     destruct st as [[[[??]?]?]|]; last by destruct Hst as [[?|] Hst]; inversion Hst.
     move:Hst=>/Some_pair_included [/Some_pair_included_total_1
               [/to_agree_included /(leibniz_equiv _ _) [= <- <-] _] _].
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 4d4e1a472f1a6c865999f0856c8d7a013ec79872..92cd71816d62f1cb35f97c37970859ec56447b34 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree excl.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing.
@@ -128,7 +128,8 @@ Section rwlock.
         iExists κ, γ. iSplitR. by iApply lft_incl_refl. iApply bor_share; try done.
         solve_ndisj. }
     clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
-    - iFrame. iMod (own_alloc (● None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
+    - iFrame. iMod (own_alloc (● None)) as (γ) "Hst"; first by apply auth_auth_valid.
+      iExists γ, None. by iFrame.
     - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
       iMod (own_alloc (● Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γ) "Hst".
       { by apply auth_auth_valid. }
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index fccc7cea67ba6ebde98f749712bd09606c827129..0cca47c4e3af7cbfcea498e45b50da2af0164b44 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -87,7 +87,7 @@ Section rwlockreadguard_functions.
                (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid lx' γ β ty))%I
         with "[H● H◯ Hx' Hν Hst H†]" as "INV".
       { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
-           %option_included Hv]%auth_valid_discrete_2.
+           %option_included Hv]%auth_both_valid.
         - destruct st0 as [|[[agν q']n]|]; try by inversion Heq. revert Heq. simpl.
           intros [[EQ <-%leibniz_equiv]%(inj2 pair) <-%leibniz_equiv]
                  %(inj Cinr)%(inj2 pair).
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index b9c9010aa835b33b496cda96571a4e83ef6f6e5f..0646d740d19572cf0df3009721090a32730e649d 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -126,7 +126,7 @@ Section rwlockwriteguard_functions.
     iDestruct "INV" as (st) "(H↦ & H● & INV)". wp_write.
     iMod ("Hcloseβ" with "[> H↦ H● H◯ INV Hx']") as "Hβ".
     { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> &
-         [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2;
+         [Heq|Hle])]%option_included Hv]%auth_both_valid;
       last by destruct (exclusive_included _ _ Hle).
       destruct st0 as [[[]|]| |]; try by inversion Heq.
       iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.