diff --git a/opam b/opam
index 36332e3acd7eba971dac4caa07a7e5b9512cdd96..eb9277d056804de96ae9689a09b2a8b441b7d743 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-09-15.0.f118e18e") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-09-30.0.50bc07aa") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index f0c472fdae2bd5eb0c62ec0ce313073e99939c71..43454d356d152ac04bcf41f886534bc503381ed2 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -606,10 +606,10 @@ Section arc.
       rewrite -5!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
                           (prodUR (prodUR move_selfUR move_otherUR) move_otherUR)).
       rewrite /= -2!pair_op /= !left_id /=. split.
-      { by split; apply auth_both_valid. }
+      { by split; apply auth_both_valid_discrete. }
       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]);
+      split; split; [..|by apply auth_both_valid_discrete|by apply auth_auth_valid];
+        (split; [by apply auth_both_valid_discrete|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])".
@@ -663,10 +663,10 @@ Section arc.
       rewrite -4!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
                           (prodUR (prodUR move_selfUR move_otherUR) move_otherUR)).
       rewrite /= -2!pair_op /= !left_id /=. split.
-      { by split; apply auth_both_valid. }
+      { by split; apply auth_both_valid_discrete. }
       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]);
+      split; split; [..|by apply auth_both_valid_discrete|by apply auth_auth_valid];
+        (split; [by apply auth_both_valid_discrete|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]";
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index ce111fe8d0b2244637bd8fdb812f1b79fe98a0d9..b0c3e88cd7798d4d01fbaa81fc4f31677748e96d 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -195,14 +195,14 @@ Section ArcGhost.
     ✓ (moveSAuth Mt1 ⋅ moveSMain q Mt2) → Mt2 = Mt1.
   Proof.
     rewrite -pair_op right_id.
-    move => [/= /auth_both_valid [/Some_included
+    move => [/= /auth_both_valid_discrete [/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_both_valid [/latT_included // _]]]. Qed.
+  Proof. rewrite -pair_op => [[_ /auth_both_valid_discrete [/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_both_valid [/Some_included
+    move => [/= /auth_both_valid_discrete [/Some_included
               [[/= _ /to_latT_inj /leibniz_equiv_iff //]|
               /prod_included [/= /frac_included /= // _]]]].
   Qed.
@@ -268,7 +268,7 @@ Section ArcGhost.
     ✓ (moveOAuth Mt1 ⋅ certO Mt2) → Mt2 ⊆ Mt1.
   Proof.
     rewrite -pair_op right_id.
-    move => [/= _ /auth_both_valid [/latT_included // ]].
+    move => [/= _ /auth_both_valid_discrete [/latT_included // ]].
   Qed.
 
   Lemma StrongDownAuth_agree γ Dt Dt':
@@ -397,7 +397,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. iIntros "oA".
     iDestruct (own_valid with "oA")
-      as %[[[[|INCL]%option_included _]%auth_both_valid _] _]; [done|].
+      as %[[[[|INCL]%option_included _]%auth_both_valid_discrete _] _]; [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_both_valid] _].
+      as %[[_ [[_ INCL]%prod_included VALID]%auth_both_valid_discrete] _].
     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_both_valid] _].
+    iDestruct (own_valid with "own") as %[[_ [VAL _]%auth_both_valid_discrete] _].
     iPureIntro. move : VAL => /prod_included /= [/option_included [//|[?[? [?[??]]]]] _].
     subst iS. by eexists.
   Qed.
@@ -608,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_both_valid] _];
+      as %[[_ [[_ [?|INCL]%option_included]%prod_included [_ VAL]]%auth_both_valid_discrete] _];
       [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 cf5ab66f4a3f467f165426694dfbdefa06ec2385..3073b4d2ca88d3eba3cf73055a55cb3e4492bfe8 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -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_both_valid.
+    as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
   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_both_valid.
+    as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
   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_l _]%auth_both_valid.
+        %[(s0 & Hv & Hincl)%singleton_included_l _]%auth_both_valid_discrete.
     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_l _]%auth_both_valid.
+        as %[(s & HA' & [Hs|Hs]%Some_included)%singleton_included_l _]%auth_both_valid_discrete.
       - 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'=>//.
@@ -171,7 +171,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_l _]%auth_both_valid.
+      as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
     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 _)]. }
@@ -273,7 +273,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_l _]%auth_both_valid.
+      as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
     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 _)]. }
@@ -281,7 +281,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_both_valid.
+    as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
   iDestruct (slice_delete_empty _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
     by rewrite lookup_fmap EQB.
   iMod (slice_insert_empty _ _ true _ Q with "Hbox") as (j) "(% & #Hs' & Hbox)".
@@ -353,7 +353,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_both_valid.
+      as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
   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_sep.v b/theories/lifetime/model/borrow_sep.v
index fdfbddf59d9f46a4d56af11a3c4badfc10107abd..f10112f59fc89e3c0973806654d9001022f3f23d 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -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_both_valid.
+      as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
   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_both_valid.
+      as %[EQB1%to_borUR_included _]%auth_both_valid_discrete.
   iDestruct (own_bor_valid_2 with "Hown Hbor2")
-      as %[EQB2%to_borUR_included _]%auth_both_valid.
+      as %[EQB2%to_borUR_included _]%auth_both_valid_discrete.
   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 772c9b7cc9f0385be4d2e95c7bf8b6107afba039..4a3ac825892c0134787962bd2146f6a05f0bbf67 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -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_both_valid; by inversion_clear EQ.
+  iDestruct 1 as %[[[[]|] EQ%(inj Some)] _]%auth_both_valid_discrete; 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)) : _ -d> _)))) (dom _ f))
-    as (γ) "[Hdom Hγ]". { split; [by apply auth_both_valid|done]. }
+    as (γ) "[Hdom Hγ]". { split; [by apply auth_both_valid_discrete|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 c3525888f46f3b07ef4ceb5c43e95f505393412a..244e3ddb56c57ee559fe6ca1f4e76f746132d878 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -33,7 +33,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_both_valid; lia. }
+      as %[?%nat_included _]%auth_both_valid_discrete; 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)".
@@ -184,7 +184,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_l Hv]%auth_both_valid.
+    as %[[s [Hs Hincl%Some_included]]%singleton_included_l Hv]%auth_both_valid_discrete.
   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/faking.v b/theories/lifetime/model/faking.v
index 23f13c27da42cfa91c6f7015fb042fda1aef5491..112cdaa87304d80528d0fa071ea8213b1404eea4 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -15,9 +15,9 @@ 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 by apply auth_both_valid.
+  iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid_discrete.
   iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name (excl (bor_state Lat)))))
-    as (γbor) "[Hbor Hbor']"; first by apply auth_both_valid.
+    as (γbor) "[Hbor Hbor']"; first by apply auth_both_valid_discrete.
   iMod (own_alloc ((● ε) :auth (gset_disj slice_name)))
      as (γinh) "Hinh"; first by apply auth_auth_valid.
   set (γs := LftNames γbor γcnt γinh).
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index fb9343ca3971cd1f3a6665b972252cef90ba1b75..999912e1933f9521cdae3ecf137f1b6f8666e398 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -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_l _]%auth_both_valid.
+    as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid_discrete.
   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_both_valid.
+  iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid_discrete.
   iPureIntro. move: HA=> /singleton_included_l [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.
@@ -456,7 +456,7 @@ Proof.
   { 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_both_valid.
+    as %[Hle%gset_disj_included _]%auth_both_valid_discrete.
   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 6f79fbc2e0a0c900143f4d243773d0a081c84e01..15ce9b6f7d4ae135499a1ca9e1e0ccea72cd7272 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -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_both_valid.
+    as %[HB%to_borUR_included _]%auth_both_valid_discrete.
   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_both_valid.
+    as %[HB%to_borUR_included _]%auth_both_valid_discrete.
   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_both_valid.
+    as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
   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 a50131a61ea65bd21dadd6fbba186a29eb14eed0..5dc181dccf5f76f1a6118c02f2bfc65d56c56d2a 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -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_both_valid. }
+        { by apply auth_both_valid_discrete. }
         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_acc 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_both_valid.
+        %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
       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_acc 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_both_valid.
+            %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
           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_both_valid;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     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_both_valid;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     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_both_valid;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
       apply csum_included in Hincl. naive_solver. }
@@ -1078,7 +1078,7 @@ Section code.
       { 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]";
-          first by apply auth_both_valid.
+          first by apply auth_both_valid_discrete.
         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 798b16c70dfe660ae082e51b8ef8e878537a7dc2..eadb9ca551a6a12dc60649e1c91af06e1aea4e7c 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_both_valid.
+      %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
     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_both_valid;
+               %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     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_both_valid.
+        %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
       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_acc 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_both_valid.
+          %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
       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_both_valid. by split. }
+      { apply auth_both_valid_discrete. 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 c76a26347bf0098658cc965276b2cd8c5736312c..f8d64e9fc4e162694c8e468dd0b3ad75aae4a493 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_both_valid; simpl in *; subst.
+               %option_included Hv]%auth_both_valid_discrete; 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_both_valid.
+              %Some_included _]%auth_both_valid_discrete.
       - 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/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index d54884597af255b162a4444211b07067939b48ea..57f781da73844ac668d92ddbb4b843e6b808cca3 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_both_valid.
+         %auth_both_valid_discrete.
       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_both_valid.
+    iDestruct (own_valid_2 with "H● Hγ") as %[Hst _]%auth_both_valid_discrete.
     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 2dab818e348ecb5c5bfc8aa723c84548b6f50adc..de3da62e791d565edee31bfd62baf35a28cb7984 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -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_both_valid.
+    iDestruct (own_valid with "mr") as %[INCL VAL]%auth_both_valid_discrete.
     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_both_valid.
+    iDestruct (own_valid with "mw") as %[INCL VAL]%auth_both_valid_discrete.
     iPureIntro. destruct st as [[[]|[[]]]|]; [done|..].
     - move : INCL =>
         /Some_included [Eq|/csum_included [//|[[?[?[?[Eq _]]]]|[?[?[?[??//]]]]]]];