diff --git a/opam b/opam
index 9783eaff6b9d8470fc1572a1b58cf4d0821e12bf..5fc43fad2d1a5843f29a02c9e25f19ad2586945a 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2019-05-15.0.7cf08612") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-05-24.0.2deb7cf6") | (= "dev") }
 ]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 63364659e06f1c18defce8b6d10ea661f4d33dfe..2a5e332bb1dfe4fad95764b0ddc8ba31bcb8ef1f 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -604,11 +604,12 @@ Section arc.
       iMod (own_alloc (A:=arcUR)) as (γ) "Own"; last by iExists γ.
       rewrite 5!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
                           (prodUR (prodUR move_selfUR move_otherUR) move_otherUR)).
-      rewrite /=. split; [done|]. rewrite 2!pair_op 2!right_id_L.
-      rewrite /= 3!left_id right_id. do 2 setoid_rewrite pair_op.
-      rewrite /= 9!left_id_L right_id_L. split; split; simpl; try done.
-      by rewrite 3!left_id pair_op 2!right_id_L right_id /=.
-      by rewrite left_id pair_op right_id_L. by rewrite /= right_id_L. }
+      rewrite /= 2!pair_op /= !left_id /=. split.
+      { by split; apply auth_both_valid. }
+      do 2 setoid_rewrite pair_op. rewrite /= !left_id !right_id.
+      split; split; [..|by apply auth_both_valid|by apply auth_auth_valid];
+        (split; [by apply auth_both_valid|rewrite /= right_id]);
+        [|rewrite left_id]; by apply auth_auth_valid. }
     iDestruct "Own" as (γsw)
       "(SA & St & WA & SMA & [SM1 SM2] & SDA & [SD1 SD2] & WUA & WU & [S1 S2])".
     iMod (view_inv_alloc_frac N _ (1/2 + 1/2/2) (1/2/2)) as (γi) "[[tok2 tok1] VI]";
@@ -660,10 +661,12 @@ Section arc.
       iMod (own_alloc (A:=arcUR)) as (γ) "?"; last by iExists γ.
       rewrite 4!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
                           (prodUR (prodUR move_selfUR move_otherUR) move_otherUR)).
-      rewrite /=. split; [done|]. rewrite 2!pair_op 2!right_id_L /= 3!left_id.
-      do 2 setoid_rewrite pair_op. rewrite /= 4!left_id_L right_id_L 4!left_id.
-      split; split; simpl; try done. by rewrite right_id pair_op right_id_L.
-      by rewrite left_id_L pair_op right_id_L. by rewrite right_id_L 3!left_id_L. }
+      rewrite /= 2!pair_op /= !left_id /=. split.
+      { by split; apply auth_both_valid. }
+      do 2 setoid_rewrite pair_op. rewrite /= !left_id !right_id.
+      split; split; [..|by apply auth_both_valid|by apply auth_auth_valid];
+        (split; [by apply auth_both_valid|rewrite /= right_id]);
+        [|rewrite left_id]; by apply auth_auth_valid. }
     iDestruct "Own" as (γsw) "(SA & WA & Wt & SMA & SM & SDA & SD & WUA & [WU1 WU2])".
     iMod (view_inv_alloc_frac N _ (1/2 + 1/2/2) (1/2/2)) as (γi) "[[tok2 tok1] VI]";
       first by rewrite -Qp_plus_assoc 2!Qp_div_2.
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 05368e4a112507687f8bbff87651b774e675a010..6d6871a6da008597b4f41881a850a5b854e81df4 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -194,15 +194,15 @@ Section ArcGhost.
   Lemma arc_ghost_move_self_main_valid Mt1 Mt2 q:
     ✓ (moveSAuth Mt1 ⋅ moveSMain q Mt2) → Mt2 = Mt1.
   Proof.
-    rewrite pair_op right_id_L.
-    move => [/= /auth_valid_discrete_2 [/Some_included
+    rewrite pair_op right_id.
+    move => [/= /auth_both_valid [/Some_included
             [[_ /= /to_agree_inj /to_latT_inj /leibniz_equiv_iff //]|
               /prod_included[_ /to_agree_included /to_latT_inj /leibniz_equiv_iff //]]_]_].
   Qed.
 
   Lemma arc_ghost_move_self_cert_valid Mt1 Mt2:
     ✓ (moveSAuth Mt1 ⋅ certS Mt2) → Mt2 ⊆ Mt1.
-  Proof. rewrite pair_op => [[_ /auth_valid_discrete_2 [/latT_included // _]]]. Qed.
+  Proof. rewrite pair_op => [[_ /auth_both_valid [/latT_included // _]]]. Qed.
 
   Lemma StrongMoveAuth_agree γ Mt q Mt':
     StrongMoveAuth γ Mt ∗ StrMoves γ q Mt' -∗ ⌜Mt = Mt'⌝.
@@ -259,7 +259,7 @@ Section ArcGhost.
     ✓ (moveOAuth Mt1 ⋅ moveOMain 1%Qp Mt2) → Mt2 = Mt1.
   Proof.
     rewrite pair_op.
-    move => [/= /auth_valid_discrete_2 [/Some_included
+    move => [/= /auth_both_valid [/Some_included
               [[/= _ /to_latT_inj /leibniz_equiv_iff //]|
               /prod_included [/= /frac_included /= // _]]]].
   Qed.
@@ -267,8 +267,8 @@ Section ArcGhost.
   Lemma arc_ghost_move_other_cert_valid Mt1 Mt2:
     ✓ (moveOAuth Mt1 ⋅ certO Mt2) → Mt2 ⊆ Mt1.
   Proof.
-    rewrite pair_op right_id_L.
-    move => [/= _ /auth_valid_discrete_2 [/latT_included // ]].
+    rewrite pair_op right_id.
+    move => [/= _ /auth_both_valid [/latT_included // ]].
   Qed.
 
   Lemma StrongDownAuth_agree γ Dt Dt':
@@ -342,7 +342,7 @@ Section ArcGhost.
     apply prod_update; [|rewrite /= !right_id //].
     setoid_rewrite pair_op. rewrite /=.
     apply prod_update; [rewrite /= !right_id //|].
-    rewrite /= 2!pair_op /= 2!right_id_L left_id_L. rewrite -2!lat_op_join'.
+    rewrite /= 2!pair_op /= 2!right_id left_id. rewrite -2!lat_op_join'.
     apply prod_update; simpl.
     - apply auth_update, option_local_update, prod_local_update_2.
       rewrite (cmra_comm_L (to_latT Dt1)) (cmra_comm_L (to_latT Dt2)).
@@ -385,7 +385,7 @@ Section ArcGhost.
     - apply auth_update, option_local_update, prod_local_update_2.
       rewrite -2!lat_op_join' (cmra_comm_L (to_latT Ut1)) (cmra_comm_L (to_latT Ut2)).
       by apply op_local_update_discrete.
-    - rewrite -lat_op_join' right_id_L left_id_L. apply auth_update_alloc.
+    - rewrite -lat_op_join' right_id left_id. apply auth_update_alloc.
       rewrite cmra_comm_L -{2}(right_id_L ε op (to_latT Ut')).
       by apply op_local_update_discrete.
   Qed.
@@ -397,7 +397,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. iIntros "oA".
     iDestruct (own_valid with "oA")
-      as %[[[[|INCL]%option_included _]%auth_valid_discrete_2 _] _]; [done|].
+      as %[[[[|INCL]%option_included _]%auth_both_valid _] _]; [done|].
     iPureIntro. destruct INCL as [q1 [[q' n] [Eq1 [Eq2 Eq3]]]].
     inversion Eq1. subst q1. exists q', n. split; [done|].
     destruct Eq3 as [[Eq3 Eq4]|[[q'' Le1] Le2%pos_included]%prod_included].
@@ -413,7 +413,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. iIntros "oA".
     iDestruct (own_valid with "oA")
-      as %[[_ [[_ INCL]%prod_included VALID]%auth_valid_discrete_2] _].
+      as %[[_ [[_ INCL]%prod_included VALID]%auth_both_valid] _].
     iPureIntro. destruct st as [st' st]. simpl in *.
     apply option_included in INCL as [|[q1 [qn [Eq1 [Eq2 Eq3]]]]]; [done|].
     subst st. inversion Eq1. subst q1. destruct Eq3 as [Eq3|INCL].
@@ -539,7 +539,7 @@ Section ArcGhost.
     WeakAuth γ (iS, st) ∗ agown γ (awk_n ((Some q, ε))) -∗ ∃ q', ⌜iS = Some q'⌝.
   Proof.
     rewrite -embed_sep -own_op. iIntros "own".
-    iDestruct (own_valid with "own") as %[[_ [VAL _]%auth_valid_discrete_2] _].
+    iDestruct (own_valid with "own") as %[[_ [VAL _]%auth_both_valid] _].
     iPureIntro. move : VAL => /prod_included /= [/option_included [//|[?[? [?[??]]]]] _].
     subst iS. by eexists.
   Qed.
@@ -548,8 +548,9 @@ Section ArcGhost.
     WeakAuth γ (iS, st) -∗ ⌜st ≠ Some CsumBot⌝.
   Proof.
     iIntros "own".
-    iDestruct (@own_valid _ arcUR with "own") as %[[_ [_ [_ VAL]]%auth_valid_discrete] _].
-    simpl in VAL. iPureIntro. by destruct st as [[| |]|].
+    iDestruct (@own_valid _ arcUR with "own") as %[[_ Hvl] _].
+    iPureIntro. move : Hvl. rewrite auth_auth_valid => [[_ ?]].
+    by destruct st as [[| |]|].
   Qed.
 
   Lemma WeakAuth_drop_strong γ st:
@@ -607,7 +608,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. iIntros "own".
     iDestruct (@own_valid _ arcUR with "own")
-      as %[[_ [[_ [?|INCL]%option_included]%prod_included [_ VAL]]%auth_valid_discrete_2] _];
+      as %[[_ [[_ [?|INCL]%option_included]%prod_included [_ VAL]]%auth_both_valid] _];
       [done|]. iPureIntro.
     destruct INCL as (x & y & Eq1 & Eq2 & INCL). simpl in *. inversion Eq1.
     subst x st. destruct INCL as [Eq|INCL].
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 3ae7fd4ecc5a61bc339fc878cd7efa2329e96efe..ac0ae54f868a29a4d85cb2ee214257207cd8b78e 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset.
 Set Default Proof Using "Type".
 
 Section accessors.
@@ -18,7 +18,7 @@ Proof.
   iIntros (?) "Hslice Halive Hbor Htok". rewrite /lft_bor_alive /idx_bor_own.
   iDestruct "Halive" as (B) "[[Hbox >Hown] HB]". iDestruct "Hbor" as (V') "[% Hbor]".
   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 "[HP Hbox]".
     solve_ndisj. by rewrite lookup_fmap EQB.
   rewrite -(fmap_insert bor_filled _ _ (Bor_open q Vtok V')).
@@ -39,7 +39,7 @@ Proof.
   iIntros (? HVV') "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 (Vtok' ⊔ V))).
@@ -78,7 +78,7 @@ Proof.
     [by rewrite Hf2 Hf1|by apply Hhv2, Hhv1].
   - clear. iIntros (Λ HΛ A) "Htok HA". iDestruct "Htok" as (V') "[% Htok]".
     iDestruct (own_valid_2 with "HA Htok") as
-        %[(s0 & Hv & Hincl)%singleton_included _]%auth_valid_discrete_2.
+        %[(s0 & Hv & Hincl)%singleton_included _]%auth_both_valid.
     revert Hv Hincl. rewrite lookup_fmap. case HA: (A!!Λ)=>[[b V'']|]; [|by inversion 1].
     move=> <- /Some_included Hincl. destruct b; last first.
     { case Hincl=>[|/csum_included]; [by inversion 1|]. naive_solver. }
@@ -101,7 +101,7 @@ Proof.
     iAssert (⌜lft_has_view A' κ V⌝)%I as %HA'V.
     { iIntros (Λ HΛ). iDestruct (@big_sepMS_elem_of with "Htok") as "Htok"=>//.
       iDestruct (own_valid_2 with "HA' Htok")
-        as %[(s & HA' & [Hs|Hs]%Some_included)%singleton_included _]%auth_valid_discrete_2.
+        as %[(s & HA' & [Hs|Hs]%Some_included)%singleton_included _]%auth_both_valid.
       - setoid_subst. rewrite lookup_fmap /to_lft_stateR in HA'.
         destruct (A'!!Λ) as [[[] V']|]=>/=.
         + apply (inj Some), (inj Cinl), (inj2 pair), proj2, (inj to_latT) in HA'=>//.
@@ -170,7 +170,7 @@ Proof.
   iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
   { 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.
     exfalso. destruct INCL as [[=]|(? & ? & [=<-] & Hi & Ho)].
     rewrite lookup_fmap in Hi. destruct (B !! s); inversion Hi; subst; clear Hi.
     by destruct Ho as [?%(inj Excl)|?%(exclusive_included _)]. }
@@ -271,7 +271,7 @@ Proof.
   iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
   { 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.
     exfalso. destruct INCL as [[=]|(? & ? & [=<-] & Hi & Ho)].
     rewrite lookup_fmap /= in Hi. destruct (B !! s''); inversion Hi; subst; clear Hi.
     by destruct Ho as [?%(inj Excl)|?%(exclusive_included _)]. }
@@ -279,7 +279,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.
   iDestruct (slice_delete_empty _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
     by rewrite lookup_fmap EQB.
   iMod (slice_insert_empty _ _ true with "Hbox") as (j) "(% & #Hs' & Hbox)".
@@ -351,7 +351,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_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
     solve_ndisj. by rewrite lookup_fmap EQB.
   iApply fupd_frame_l. iSplitL "HP'".
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 061f6f807b0555b0ae195c93e3e4a0676d4fa336..427bd7559ca69bc0f484ba3864d94a4f08120537 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Export faking.
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 65f6a86e0e7c0f65c3474cf83a8867ff5aa7106e..40f75c835a38073b387f77814d062eb2e6ec6b6e 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Export faking reborrow.
-From iris.algebra Require Import csum auth frac gmap agree.
+From iris.algebra Require Import csum auth excl frac gmap agree.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
@@ -55,7 +55,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.
   iAssert (▷ ⌜V' ⊑ Vκ⌝)%I with "[#]" as ">%".
   { iNext. rewrite big_sepM_lookup //. simpl. by iDestruct "HB" as %?. }
   iMod (slice_delete_full _ _ true with "Hslice Hbox")
@@ -149,9 +149,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.
   { iIntros (->).
     iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 898e1e29964e0172fb7f624bf9c3a5bcd93618f8..2c2741cc0d89db3fecaba0c18c5d6f9fce3be708 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -1,5 +1,5 @@
 From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Import auth gmap agree.
+From iris.algebra Require Import auth gmap agree excl.
 From iris.bi Require Import big_op.
 From iris.proofmode Require Import tactics.
 From gpfsl.base_logic Require Import vprop lattice_cmra.
@@ -94,7 +94,7 @@ Lemma box_own_auth_agree γ o1 o2 :
   box_own_auth γ (● Excl' o1) ∗ box_own_auth γ (◯ Excl' o2) ⊢ o1 ≡ o2.
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
-  iDestruct 1 as %[[[[]|] EQ%(inj Some)] _]%auth_valid_discrete; by inversion_clear EQ.
+  iDestruct 1 as %[[[[]|] EQ%(inj Some)] _]%auth_both_valid; by inversion_clear EQ.
 Qed.
 
 Lemma box_own_auth_update γ o1 o2 o3 :
@@ -126,7 +126,7 @@ Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iMod (own_alloc_cofinite (● Excl' None ⋅ ◯ Excl' None,
     Some (to_agree (Next ((λ V, iProp_unfold (Q V)) : _ -c> _)))) (dom _ f))
-    as (γ) "[Hdom Hγ]"; first done.
+    as (γ) "[Hdom Hγ]". { split; [by apply auth_both_valid|done]. }
   rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
   iDestruct "Hdom" as % ?%not_elem_of_dom.
   iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 5e9d45b8868871bda57fe4d6c99119e1575a56d7..3e186017ab5f92f7f863ef9b8fc8339f937ee103 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"; [by apply HK|].
     rewrite /lft_inv_dead; iDestruct "Hdead" as (R Vinh) "(_ & _ & 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 (Vκ n) "(% & Hcnt & Hvs)".
@@ -183,7 +183,7 @@ Proof.
   iDestruct "H" as (A I) "(% & HA & HI & Hinv)".
   rewrite /lft_tok /= big_sepMS_singleton. iDestruct "HΛ" as (V'0) "[#HV'0 HΛ]".
   iDestruct (own_valid_2 with "HA HΛ")
-    as %[[s [Hs Hincl%Some_included]]%singleton_included Hv]%auth_valid_discrete_2.
+    as %[[s [Hs Hincl%Some_included]]%singleton_included Hv]%auth_both_valid.
   destruct Hincl; last first.
   { destruct (exclusive_included (Cinl (1%Qp, to_latT V'0)) s)=>//.
     move: (Hv Λ). by rewrite Hs. }
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 94bed26c60bbc86de4c0fb9e38f1267e29a2c1e2..9dde6009d7b0b97b79096f3d1492e3994d8ca54e 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset.
 From lrust.lifetime.model Require Import boxes.
 From lrust.lifetime Require Export lifetime_sig.
 From gpfsl.base_logic Require Export lattice_cmra.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 0e0016824c416ab60f386f69c0ea43ab3714612e..0704936e5dbd789a3d396700031b36692831765b 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -1,5 +1,5 @@
 From lrust.lifetime.model Require Export primitive.
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
@@ -15,11 +15,11 @@ Proof.
   iIntros "HA HI Hinv".
   destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
   { iModIntro. iExists A, I. iFrame. iPureIntro. by apply elem_of_dom. }
-  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 (excl (bor_state Lat)))))
-    as (γbor) "[Hbor Hbor']"; first by apply auth_valid_discrete_2.
+    as (γbor) "[Hbor Hbor']"; 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 7c8d9c738c5da474a840b06ce5eadb119e3b6971..843edb0d04b08ce044bc77c6e3ac4e76ba50865a 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import csum auth frac gmap agree gset proofmode_classes.
+From iris.algebra Require Import csum auth excl frac gmap agree gset proofmode_classes.
 From iris.bi Require Import big_op fractional.
 From iris.proofmode Require Import tactics.
 From lrust.lifetime.model Require Export definitions boxes.
@@ -9,8 +9,8 @@ Lemma lft_init `{!invG Σ, !lftPreG Lat Σ} E E0 :
   ↑lftN ⊆ E → ↑lftN ## E0 → (|={E}=> ∃ _ : lftG Lat E0 Σ, lft_ctx)%I.
 Proof.
   iIntros (? HE0). rewrite /lft_ctx.
-  iMod (own_alloc (● ∅ : authR (alftUR Lat))) as (γa) "Ha"; first done.
-  iMod (own_alloc (● ∅ : authR ilftUR)) as (γi) "Hi"; first done.
+  iMod (own_alloc (● ∅ : authR (alftUR Lat))) 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 _ E0 _ _ _ γa _ γi _ _ _ HE0). iExists HlftG.
   iMod (inv_alloc _ _ lfts_inv with "[Ha Hi]") as "$"; last done.
   iModIntro. rewrite /lfts_inv /own_alft_auth /own_ilft_auth. iExists ∅, ∅.
@@ -35,7 +35,7 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
     own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜κ ∈ dom (gset _) 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.
   iPureIntro. apply elem_of_dom. unfold to_ilftUR in *. simplify_map_eq.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.
@@ -45,7 +45,7 @@ Lemma own_alft_auth_agree (A : gmap atomic_lft (bool * Lat)) Λ bV :
     own alft_name (◯ {[Λ := to_lft_stateR bV]}) -∗ ⌜A !! Λ ≡ Some bV⌝.
 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 []].
   rewrite lookup_fmap fmap_Some_equiv=> -[bV' [-> ->]] /Some_included [EQ|/csum_included].
   - destruct bV as [[]?], bV' as [[]?]; (try by inversion EQ); do 2 f_equiv.
@@ -69,8 +69,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_valid op_singleton singleton_valid=> /agree_op_invL' <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_sep κ x x1 x2 :
@@ -101,14 +101,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_valid op_singleton singleton_valid=> /agree_op_invL' <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_cnt_into_sep κ 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.
@@ -135,14 +135,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_sep κ 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.
@@ -289,7 +289,7 @@ Proof.
   iDestruct 1 as (Λ' V')  "(% & #? & H')".
   iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //.
   iDestruct "H" as (V'') "[#? 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.
@@ -451,12 +451,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 3b42ad682b22b40ee972c7fb346f66657564b2bd..bba7a7df4668189deb9addb6810f8617a931085c 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -1,5 +1,5 @@
 From lrust.lifetime Require Import borrow accessors.
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
@@ -24,8 +24,8 @@ Proof.
   rewrite bi.sep_and -(assoc bi_and) (and_extract_own _ _ P).
   iIntros "(#Hag & Hσ & Hclose)". iSplitL "Hσ"; [by auto|]. iIntros "H".
   iApply "Hclose". iDestruct "H" as (γ') "[#Hag' H]".
-  iDestruct (own_valid_2 with "Hag Hag'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL' <- //.
+  iDestruct (own_valid_2 with "Hag Hag'") as %Hγs. move : Hγs.
+  rewrite auth_frag_valid op_singleton singleton_valid=> /agree_op_invL' <- //.
 Qed.
 
 Section reborrow.
@@ -65,7 +65,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]".
@@ -112,7 +112,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.
   iAssert ⌜V0 ⊑ Vs κ⌝%I with "[#]" as "%".
   { rewrite (big_sepM_lookup _ _ _ _ HB) /=. iDestruct "HB" as "[$  _]". }
   iAssert (∃ VP, ⌜VP ⊑ Vs κ⌝ ∗ ▷ Q (Vs κ') ∗ ▷ P VP ∗
@@ -173,7 +173,7 @@ Proof.
   iDestruct "Halive" as (B) "[[Hbox >H●] HB]". rewrite [_ (κ', i')]/idx_bor_own.
   iDestruct "Hbor" as (V') "[#HV' Hbor]".
   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 (▷ ⌜κ ∈ dom (gset lft) I⌝)%I with "[#]" as ">%".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index e0f876addc3ec03fde1f25100549d1361bcbbcfd..8401a501e809294e0294a147a579585143c60ae5 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1,5 +1,5 @@
 From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth excl csum frac agree.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
@@ -164,7 +164,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 "Ha". iExists _.
@@ -289,7 +289,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].
@@ -348,7 +348,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 _. }
@@ -419,7 +419,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. }
@@ -478,7 +478,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. }
@@ -583,7 +583,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. }
@@ -1077,7 +1077,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 ea17f33885235f09d93b283d5aa5e689b3f4f3a8..051166aeb67fe0e23c8b8e2b61d07de7596d6e94 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -164,7 +164,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ν†)".
@@ -267,7 +267,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. }
@@ -333,7 +333,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). }
@@ -406,7 +406,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,
@@ -479,7 +479,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 2d368942963eb6fff536e571d11a461233ac3479..d89fc965fb8d5fa96a37a06ba653ae7b1d30bb03 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -25,7 +25,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
@@ -165,7 +165,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 4b97cb064902ace43b609131742dda1dfd604bc0..43924772517b9a634ef435e9c642fd1642c628ee 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -136,7 +136,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 0610118a3fc7b1cf25cd4611baf264d68dfda25c..4b34ab08d44fef54cfaa5381c978828507f13254 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -130,7 +130,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].
@@ -298,7 +298,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 b2166089f1004bcf0f4123102b740d62e6bc8911..ad4b117eb2e849078727925466826265e07dbcfd 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.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 excl csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing.
@@ -107,7 +107,7 @@ Section rwlock_inv.
         ∨ (∃ q0, q' = (q + q0)%Qp) ∧ n = (1 + Pos.pred n)%positive)⌝.
   Proof.
     iIntros "m r". iCombine "m" "r" as "mr".
-    iDestruct (own_valid with "mr") as %[INCL VAL]%auth_valid_discrete_2.
+    iDestruct (own_valid with "mr") as %[INCL VAL]%auth_both_valid.
     iPureIntro. destruct st as [[[]|[[]]]|].
     - move : INCL =>
         /Some_included [Eq|/csum_included [//|[[?[?[??//]]]|[?[?[?[??//]]]]]]].
@@ -155,7 +155,7 @@ Section rwlock_inv.
     ⌜st = (Some (inl tt))⌝.
   Proof.
     iIntros "m w". iCombine "m" "w" as "mw".
-    iDestruct (own_valid with "mw") as %[INCL VAL]%auth_valid_discrete_2.
+    iDestruct (own_valid with "mw") as %[INCL VAL]%auth_both_valid.
     iPureIntro. destruct st as [[[]|[[]]]|]; [done|..].
     - move : INCL =>
         /Some_included [Eq|/csum_included [//|[[?[?[?[Eq _]]]]|[?[?[?[??//]]]]]]];
@@ -286,7 +286,8 @@ Section rwlock_inv.
     iAssert (|={E}=> ∃ γs, (q).[α] ∗ &{α} (∃ v, l ↦{1} v ∗ P γs v))%I
       with "[H Htok' Hvl Hclose]" as "H".
     { iDestruct "H" as ([|n|[]]) "[>Hn >%]"; try lia.
-      - iMod (own_alloc (st_global None : rwlockR)) as (γs) "Hst"; [done|].
+      - iMod (own_alloc (st_global None : rwlockR)) as (γs) "Hst";
+          first by apply auth_auth_valid.
         iExists γs. iFrame "Htok'".
         iMod ("Hclose" with "[] [-]") as "[$ $]"; [..|done].
         + iIntros "!>". iDestruct 1 as (v) "[>Hl P]".