diff --git a/opam b/opam
index 0675082c57b7f4aadb327a2cd9cef2f2e1430202..13dc9bc657bac05da1886c248d9e7b1fee51ebeb 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2019-04-17.0.60d28bbb") | (= "dev") }
+  "coq-iris" { (= "dev.2019-05-24.0.c9984c7f") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/hocap/contrib_bag.v b/theories/hocap/contrib_bag.v
index ba4164bc1a8d232cda8e0f2fc9a2b54b0bf7ebaa..5f17de258a5ad0ac10f8253ca7b185f62387c092 100644
--- a/theories/hocap/contrib_bag.v
+++ b/theories/hocap/contrib_bag.v
@@ -50,7 +50,7 @@ Section proof.
     iIntros (Φ) "_ HΦ". iApply wp_fupd.
     iApply (newBag_spec b NB); eauto.
     iNext. iIntros (v γb) "[#Hbag Hcntn]".
-    iMod (own_alloc (●! ∅ ⋅ ◯! ∅)) as (γ) "[Hown Hpart]"; first done.
+    iMod (own_alloc (●! ∅ ⋅ ◯! ∅)) as (γ) "[Hown Hpart]"; first by apply auth_both_valid.
     iMod (inv_alloc NI _ (∃ X, bag_contents b γb X ∗ own γ (●! X))%I with "[Hcntn Hown]") as "#Hinv".
     { iNext. iExists _. iFrame. }
     iApply "HΦ". iModIntro. iExists _,_. iFrame "Hinv Hbag Hpart".
diff --git a/theories/lecture_notes/ccounter.v b/theories/lecture_notes/ccounter.v
index e79736eae91bbc36291d8f3d15deeb1cf931cecf..05c92609d0ee58ed7ec2f7128c32076563b65caf 100644
--- a/theories/lecture_notes/ccounter.v
+++ b/theories/lecture_notes/ccounter.v
@@ -58,7 +58,7 @@ Section ccounter.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
     wp_apply newcounter_spec; auto.
     iIntros (ℓ) "H"; iDestruct "H" as (γ₂) "[#HCnt Hown]".
-    iMod (own_alloc (●! m%nat ⋅ ◯! m%nat)) as (γ₁) "[Hγ Hγ']"; first done.
+    iMod (own_alloc (●! m%nat ⋅ ◯! m%nat)) as (γ₁) "[Hγ Hγ']"; first by apply auth_both_valid.
     iMod (inv_alloc (N .@ "counter") _ (ccounter_inv γ₁ γ₂) with "[Hγ Hown]").
     { iNext. iExists _. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index 3bc85d30a0a2cd9d21eb18199b4117fd4bf08185..f2730d2c8fe3fb690a2af0b683125c978659f655 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -29,7 +29,7 @@ Section monotone_counter.
      algebra we shall be using. The Iris library contains all the ingredients
      needed to compose this particular resource algebra from simpler components,
      however to illustrate how to define our own we will define it from scratch.
-     
+
      In the subsequent section we show how to obtain an equivalent resource
      algebra from the building blocks provided by the Iris Coq library. 
   *)
@@ -423,7 +423,7 @@ Section monotone_counter'.
   Proof.
     (* Use a simplified definition of validity for when the underlying CMRA is discrete, i.e., an RA.
        The general definition also involves the use of step-indices, which is not needed in our case. *)
-    rewrite auth_valid_discrete_2.
+    rewrite auth_both_valid.
     split.
     - intros [? _]; by apply mnat_included.
     - intros ?%mnat_included; done.
@@ -460,7 +460,7 @@ Section monotone_counter'.
     iIntros (Φ) "_ HCont".
     rewrite /newCounter -wp_fupd.
     wp_lam.
-    iMod (own_alloc (● (0%nat : mnatUR) ⋅ ◯ 0%nat)) as (γ) "[HAuth HFrac]".
+    iMod (own_alloc (● (0%nat : mnatUR) ⋅ ◯ (0%nat : mnatUR))) as (γ) "[HAuth HFrac]".
     - apply mcounterRA_valid_auth_frag'; auto.
     - wp_alloc â„“ as "Hpt".
       iMod (inv_alloc N _ (counter_inv' ℓ γ) with "[Hpt HAuth]") as "HInv".
@@ -505,7 +505,7 @@ Section monotone_counter'.
     iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
     destruct (decide (k = m)); subst.
     + wp_cas_suc.
-      iMod (own_update γ ((● m ⋅ ◯ n)) (● (S m : mnatUR) ⋅ (◯ S n)) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
+      iMod (own_update γ ((● m ⋅ ◯ n)) (● (S m : mnatUR) ⋅ (◯ (S n : mnatUR))) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
       { apply mcounterRA_update'. }
       { rewrite own_op; iFrame. }
       iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
@@ -606,7 +606,7 @@ Section ccounter.
     {{{ γ ℓ, RET #ℓ; is_ccounter γ ℓ 1 0%nat }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newCounter /=. wp_lam. wp_alloc ℓ as "Hpt".
-    iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
+    iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']"; first by apply auth_both_valid.
     iMod (inv_alloc N _ (ccounter_inv γ ℓ) with "[Hpt Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.
diff --git a/theories/logatom/elimination_stack/hocap_spec.v b/theories/logatom/elimination_stack/hocap_spec.v
index edbcf4548164bc1eb213ecae7e82c702fe07e248..9fd1134b1ab284b73b0b53757d400b9731859e65 100644
--- a/theories/logatom/elimination_stack/hocap_spec.v
+++ b/theories/logatom/elimination_stack/hocap_spec.v
@@ -165,7 +165,7 @@ Section logatom_hocap.
     iIntros (Φ) "_ HΦ". iApply wp_fupd. iApply logatom.new_stack_spec; first done.
     iIntros "!>" (γs s) "[Hstack Hcont]".
     iMod (own_alloc (● Excl' [] ⋅ ◯ Excl' [])) as (γw) "[Hs● Hs◯]".
-    { apply auth_valid_discrete_2. split; done. }
+    { apply auth_both_valid. split; done. }
     iApply ("HΦ" $! (γs, γw)). rewrite /hocap_is_stack. iFrame.
     iApply inv_alloc. eauto with iFrame.
   Qed.
@@ -212,11 +212,11 @@ Section logatom_hocap.
     iIntros (???) "Hf1 Hf2". iDestruct (own_valid_2 with "Hf1 Hf2") as %[].
   Qed.
   Next Obligation.
-    iIntros (???) "Ha1 Ha2". iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
+    iIntros (???) "Ha1 Ha2". by iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
   Qed.
   Next Obligation.
     iIntros (???) "Hf Ha". iDestruct (own_valid_2 with "Ha Hf") as
-      %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. done.
+      %[->%Excl_included%leibniz_equiv _]%auth_both_valid. done.
   Qed.
   Next Obligation.
     iIntros (???) "Hf Ha". iMod (own_update_2 with "Ha Hf") as "[? ?]".
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index abb4d4bba55221bd3009da5099048b0c311eba2a..0c8562243d6502774ef8b19149ad6f42e24791c9 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -175,7 +175,7 @@ Section stack.
     wp_apply alloc_spec; first done. iIntros (head) "Hhead". wp_let.
     wp_apply alloc_spec; first done. iIntros (offer) "Hoffer". wp_let.
     iMod (own_alloc (● Excl' [] ⋅ ◯ Excl' [])) as (γs) "[Hs● Hs◯]".
-    { apply auth_valid_discrete_2. split; done. }
+    { apply auth_both_valid. split; done. }
     iMod (inv_alloc stackN _ (stack_inv γs head offer) with "[-HΦ Hs◯]").
     { iNext. iExists None, None, _. iFrame. done. }
     wp_pures. iApply "HΦ". iFrame "Hs◯". iModIntro. iExists _, _. auto.
@@ -209,7 +209,7 @@ Section stack.
     - (* The CAS succeeded. Update everything accordingly. *)
       iMod "AU" as (l') "[Hl' [_ Hclose]]".
       iDestruct (own_valid_2 with "Hs● Hl'") as
-        %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+        %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
       iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
       { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
       iMod ("Hclose" with "Hl'") as "HΦ". iModIntro.
@@ -283,7 +283,7 @@ Section stack.
       iDestruct "Hlist" as ">%". subst stack_rep.
       iMod "AU" as (l') "[Hl' [_ Hclose]]".
       iDestruct (own_valid_2 with "Hs● Hl'") as
-        %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+        %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
       iMod ("Hclose" with "Hl'") as "HΦ".
       iSplitR "HΦ"; first by eauto 10 with iFrame.
       iIntros "!>". wp_pures. by iApply "HΦ".
@@ -305,7 +305,7 @@ Section stack.
         and we are done. *)
         iMod "AU" as (l') "[Hl' [_ Hclose]]".
         iDestruct (own_valid_2 with "Hs● Hl'") as
-          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+          %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
         destruct l as [|v' l]; simpl.
         { (* Contradiction. *) iDestruct "Hlist" as ">%". done. }
         iDestruct "Hlist" as (tail' q' rep') "[>Heq [>Htail' Hlist]]".
@@ -345,13 +345,13 @@ Section stack.
         iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hoff)".
         iMod "AUoff" as (l') "[Hl' [_ Hclose]]".
         iDestruct (own_valid_2 with "Hs● Hl'") as
-          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+          %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
         iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
         { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
         iMod ("Hclose" with "Hl'") as "HQoff".
         iMod "AU" as (l') "[Hl' [_ Hclose]]".
         iDestruct (own_valid_2 with "Hs● Hl'") as
-          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+          %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
         iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
         { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
         iMod ("Hclose" with "Hl'") as "HΦ".
diff --git a/theories/logatom/flat_combiner/misc.v b/theories/logatom/flat_combiner/misc.v
index 07ee8cc9917f5775e48358166d616a02b0012fba..b31ea9de467860acdd5d05b3f00f0bda884b7c72 100644
--- a/theories/logatom/flat_combiner/misc.v
+++ b/theories/logatom/flat_combiner/misc.v
@@ -2,7 +2,7 @@
 
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
-From iris.algebra Require Import auth frac gmap agree.
+From iris.algebra Require Import excl auth frac gmap agree.
 From iris.bi Require Import fractional.
 From iris.base_logic Require Import auth.
 
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 5a59300ed8b009db39ec2284b6fb8231368de87c..93723832e78bffcf0b8710bb9d2a4db398e6e6b6 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -160,11 +160,11 @@ Section atomic_snapshot.
     wp_alloc ly as "Hly".
     set (Excl' (v1, v2)) as p.
     iMod (own_alloc (● p ⋅ ◯ p)) as (γ1) "[Hp⚫ Hp◯]". {
-      rewrite /p. apply auth_valid_discrete_2. split; done.
+      rewrite /p. apply auth_both_valid. split; done.
     }
     set (new_timestamp 0 v1) as t.
     iMod (own_alloc (● gmap_to_UR t ⋅ ◯ gmap_to_UR t)) as (γ2) "[Ht⚫ Ht◯]". {
-      rewrite /t /new_timestamp. apply auth_valid_discrete_2.
+      rewrite /t /new_timestamp. apply auth_both_valid.
       split; first done. rewrite /gmap_to_UR map_fmap_singleton. apply singleton_valid. done.
     }
     wp_pures. iApply ("Hp" $! (γ1, γ2)).
@@ -192,7 +192,7 @@ Section atomic_snapshot.
   Proof.
     iIntros "Hγ● Hγ◯".
     iDestruct (own_valid_2 with "Hγ● Hγ◯") as
-        %[H%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+        %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
     done.
   Qed.
 
@@ -223,7 +223,7 @@ Section atomic_snapshot.
   Proof.
     iIntros "[Hγ⚫ Hγ◯]".
     iDestruct (own_valid_2 with "Hγ⚫ Hγ◯") as
-        %[H Hv]%auth_valid_discrete_2. iPureIntro. intros t x HT2.
+        %[H Hv]%auth_both_valid. iPureIntro. intros t x HT2.
     pose proof (iffLR (lookup_included (gmap_to_UR T2) (gmap_to_UR T1)) H t) as Ht.
     rewrite !lookup_fmap HT2 /= in Ht.
     destruct (is_Some_included _ _ Ht) as [? [t2 [Ht2 ->]]%fmap_Some_1]; first by eauto.
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index 156d5cac9230e5643894c349249770bdd0a585cd..2501052d0396352e570cd87fb8ccdc97a88f1d3f 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -156,7 +156,7 @@ Lemma auth_agree γ xs ys :
   own γ (● (Excl' xs)) -∗ own γ (◯ (Excl' ys)) -∗ ⌜xs = ys⌝.
 Proof.
   iIntros "Hγ● Hγ◯". by iDestruct (own_valid_2 with "Hγ● Hγ◯")
-    as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+    as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
 Qed.
 
 (** The view of the authority can be updated together with the local view. *)
@@ -223,7 +223,8 @@ Proof.
      our camera named [γ], containing the empty list. This step (and the next)
      requires the fancy update modality that was introduced earlier. *)
   iMod (own_alloc (● (Some (Excl [])) ⋅ ◯ (Some (Excl []))))
-    as (γ) "[Hγ● Hγ◯]"; (* Validity is trivial. *) first done.
+    as (γ) "[Hγ● Hγ◯]";
+    (* Validity is trivial. *) first by apply auth_both_valid.
   (* We can then allocate the invariant (with mask [N]).  Note that we can use
      [eauto 10 with iFrame] to prove [▷ stack_inv ℓ γ]. *) 
   iMod (inv_alloc N _ (stack_inv ℓ γ) with "[Hl Hγ●]")
diff --git a/theories/logrel/F_mu_ref/rules_binary.v b/theories/logrel/F_mu_ref/rules_binary.v
index 9dbbc32f313cb37f1970f9b1e88c5b9a49dccaaf..57b846f274e361d2a86aeacc40962ea8bcaf14c8 100644
--- a/theories/logrel/F_mu_ref/rules_binary.v
+++ b/theories/logrel/F_mu_ref/rules_binary.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Import lifting.
-From iris.algebra Require Import auth frac agree gmap list.
+From iris.algebra Require Import excl auth frac agree gmap list.
 From iris_examples.logrel.F_mu_ref Require Export rules.
 From iris.proofmode Require Import tactics.
 Import uPred.
@@ -65,7 +65,7 @@ Section cfg.
     iInv specN as ">Hspec" "Hclose".
     iDestruct "Hspec" as (e'' σ) "[Hown %]".
     iDestruct (@own_valid_2 with "Hown Hj")
-      as %[[?%Excl_included%leibniz_equiv _]%prod_included Hvalid]%auth_valid_discrete_2; subst.
+      as %[[?%Excl_included%leibniz_equiv _]%prod_included Hvalid]%auth_both_valid; subst.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, option_local_update,
         (exclusive_local_update _ (Excl (fill K e'))). }
@@ -93,7 +93,7 @@ Section cfg.
     iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
     destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
     iDestruct (own_valid_2 _ with "Hown Hj")
-      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_both_valid.
     subst.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, option_local_update,
@@ -117,10 +117,10 @@ Section cfg.
     rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
     iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
     iDestruct (own_valid_2 _ with "Hown Hj")
-      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_both_valid.
     subst.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
+      as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, option_local_update,
         (exclusive_local_update _ (Excl (fill K (of_val v)))). }
@@ -139,10 +139,10 @@ Section cfg.
     rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
     iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
     iDestruct (own_valid_2 _ with "Hown Hj")
-      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_both_valid.
     subst.
     iDestruct (own_valid_2 _ with "Hown Hl")
-      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
+      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, option_local_update,
         (exclusive_local_update _ (Excl (fill K Unit))). }
diff --git a/theories/logrel/F_mu_ref/soundness.v b/theories/logrel/F_mu_ref/soundness.v
index 1eda715e04b326c6b12ccf91331c9436872b9daa..bf92b9e252ceee1932215da797164c93a885490b 100644
--- a/theories/logrel/F_mu_ref/soundness.v
+++ b/theories/logrel/F_mu_ref/soundness.v
@@ -17,7 +17,7 @@ Proof.
   eapply (wp_adequacy Σ _); eauto.
   iIntros (Hinv ?).
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
+  { by apply auth_auth_valid, to_gen_heap_valid. }
   iModIntro. iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
   set (HeapΣ := (HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
   iApply (wp_wand with "[]").
diff --git a/theories/logrel/F_mu_ref/soundness_binary.v b/theories/logrel/F_mu_ref/soundness_binary.v
index b7632c672191f175ac0a0168f3b5b1726ac67fbd..5fabf6ec0d29bcd43bc1fdd5df14396938577eac 100644
--- a/theories/logrel/F_mu_ref/soundness_binary.v
+++ b/theories/logrel/F_mu_ref/soundness_binary.v
@@ -1,5 +1,5 @@
 From iris_examples.logrel.F_mu_ref Require Export context_refinement.
-From iris.algebra Require Import auth frac agree.
+From iris.algebra Require Import excl auth frac agree.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import adequacy.
 From iris_examples.logrel.F_mu_ref Require Import soundness.
@@ -16,10 +16,10 @@ Proof.
   eapply (wp_adequacy Σ); first by apply _.
   iIntros (Hinv ?).
   iMod (own_alloc (● to_gen_heap ∅)) as (γ) "Hh".
-  { apply (auth_auth_valid _ (to_gen_heap_valid _ _ ∅)). }
+  { by apply auth_auth_valid, to_gen_heap_valid. }
   iMod (own_alloc (● (Excl' e', ∅)
     ⋅ ◯ ((Excl' e', ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
-  { apply auth_valid_discrete_2. split=>//. }
+  { apply auth_both_valid. split=>//. }
   set (Hcfg := CFGSG _ _ γc).
   iMod (inv_alloc specN _ (spec_ctx ([e'], ∅)) with "[Hcfg1]") as "#Hcfg".
   { iNext. iExists e', ∅. iSplit; eauto.
@@ -38,7 +38,7 @@ Proof.
     iDestruct "Hinv" as (e'' σ) "[Hown %]".
     rewrite /tpool_mapsto /=.
     iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
-    move: Hvalid=> /auth_valid_discrete_2
+    move: Hvalid=> /auth_both_valid
       [/prod_included [Hv2 _] _]. apply Excl_included, leibniz_equiv in Hv2. subst.
     iMod ("Hclose" with "[-]") as "_".
     + iExists (#v2), σ. auto.
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
index 007a77e24e64ab4ae4c21165237b3d23d203fe10..2c4883bc49667677ef1693ba70517b1773447b3b 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
@@ -47,7 +47,7 @@ Section Stack_refinement.
     simpl. iApply wp_pure_step_later; trivial. iNext. simpl.
     iAsimpl.
     (* establishing the invariant *)
-    iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first done.
+    iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first by apply auth_auth_valid.
     set (istkG := StackG _ _ γ).
     change γ with (@stack_name _ istkG).
     change H1 with (@stack_inG _ istkG).
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v b/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
index cd2e4a9575e40ee11708f1546d4b18c2eb6bd446..99b1bb001ff0b0273c6d8a17060ae567dc85a905 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
@@ -25,7 +25,7 @@ Section Rules.
   Lemma stack_mapstos_agree l v w : l ↦ˢᵗᵏ v ∗ l ↦ˢᵗᵏ w ⊢ ⌜v = w⌝.
   Proof.
     rewrite -own_op -auth_frag_op op_singleton own_valid.
-    by iIntros (->%auth_own_valid%singleton_valid%agree_op_invL').
+    by iIntros (->%auth_frag_valid%singleton_valid%agree_op_invL').
   Qed.
 
   Program Definition StackLink_pre (Q : D) : D -n> D := λne P v,
@@ -94,7 +94,7 @@ Section Rules.
   Proof.
     iIntros "[Howns Hls] Hl".
     iDestruct (own_valid_2 with "Howns Hl")
-      as %[[az [Haz Hq]]%singleton_included _]%auth_valid_discrete_2.
+      as %[[az [Haz Hq]]%singleton_included _]%auth_both_valid.
     rewrite lookup_fmap in Haz.
     assert (∃ z, h !! l = Some z) as Hz.
     { revert Haz; case: (h !! l) => [z|] Hz; first (by eauto); inversion Hz. }
diff --git a/theories/logrel/F_mu_ref_conc/rules_binary.v b/theories/logrel/F_mu_ref_conc/rules_binary.v
index b9152d488f873f2b6b24021b517086d643ac047f..1e939ff1a956caeaa09be004b917194c4b44a74e 100644
--- a/theories/logrel/F_mu_ref_conc/rules_binary.v
+++ b/theories/logrel/F_mu_ref_conc/rules_binary.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.program_logic Require Import lifting.
-From iris.algebra Require Import auth frac agree gmap list.
+From iris.algebra Require Import excl auth frac agree gmap list.
 From iris_examples.logrel.F_mu_ref_conc Require Export rules.
 From iris.proofmode Require Import tactics.
 Import uPred.
@@ -174,7 +174,7 @@ Section cfg.
     iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose".
     iDestruct "Hrtc" as %Hrtc.
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1,
         singleton_local_update, (exclusive_local_update _ (Excl (fill K e'))). }
@@ -221,7 +221,7 @@ Section cfg.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1,
         singleton_local_update, (exclusive_local_update _ (Excl (fill K (Loc l)))). }
@@ -244,9 +244,10 @@ Section cfg.
     rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
     iDestruct (own_valid_2 with "Hown Hl") 
-      as %[[? ?%gen_heap_singleton_included]%prod_included ?]%auth_valid_discrete_2.     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
+      as %[[? ?%gen_heap_singleton_included]%prod_included ?]%auth_both_valid.
+    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (of_val v)))). }
     iFrame "Hj Hl". iApply "Hclose". iNext.
@@ -264,9 +265,9 @@ Section cfg.
     rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
+      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K Unit))). }
@@ -289,9 +290,9 @@ Section cfg.
     rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
+      as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (#â™­ false)))). }
@@ -310,9 +311,9 @@ Section cfg.
     rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
+      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (#â™­ true)))). }
@@ -405,7 +406,7 @@ Section cfg.
     iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
     assert (j < length tp) by eauto using lookup_lt_Some.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1,
diff --git a/theories/logrel/F_mu_ref_conc/soundness_binary.v b/theories/logrel/F_mu_ref_conc/soundness_binary.v
index b8fbd287644963f0196cb30f4fdd2db46c1eae92..79cab342653efd244cacac0ac844441b1467aad4 100644
--- a/theories/logrel/F_mu_ref_conc/soundness_binary.v
+++ b/theories/logrel/F_mu_ref_conc/soundness_binary.v
@@ -15,10 +15,10 @@ Proof.
   { destruct 1; naive_solver. }
   eapply (wp_adequacy Σ _); iIntros (Hinv ?).
   iMod (own_alloc (● to_gen_heap ∅)) as (γ) "Hh".
-  { apply (auth_auth_valid _ (to_gen_heap_valid _ _ ∅)). }
+  { by apply auth_auth_valid, to_gen_heap_valid. }
   iMod (own_alloc (● (to_tpool [e'], ∅)
     ⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
-  { apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. }
+  { apply auth_both_valid. split=>//. split=>//. apply to_tpool_valid. }
   set (Hcfg := CFGSG _ _ γc).
   iMod (inv_alloc specN _ (spec_inv ([e'], ∅)) with "[Hcfg1]") as "#Hcfg".
   { iNext. iExists [e'], ∅. rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
@@ -36,7 +36,7 @@ Proof.
   iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
   rewrite /tpool_mapsto /=.
   iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
-  move: Hvalid=> /auth_valid_discrete_2
+  move: Hvalid=> /auth_both_valid
     [/prod_included [/tpool_singleton_included Hv2 _] _].
   destruct tp as [|? tp']; simplify_eq/=.
   iMod ("Hclose" with "[-]") as "_"; [iExists (_ :: tp'), σ; auto|].
diff --git a/theories/logrel/F_mu_ref_conc/soundness_unary.v b/theories/logrel/F_mu_ref_conc/soundness_unary.v
index 35798af5a8417e25de92714a3c07dbc5e6ffc3a8..293c606c8a99425e9a529d032fe2005483c73640 100644
--- a/theories/logrel/F_mu_ref_conc/soundness_unary.v
+++ b/theories/logrel/F_mu_ref_conc/soundness_unary.v
@@ -16,7 +16,7 @@ Proof.
   intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
   eapply (wp_adequacy Σ _). iIntros (Hinv ?).
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
+  { by apply auth_auth_valid, to_gen_heap_valid. }
   iModIntro. iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
   set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
   iApply (wp_wand with "[]").
diff --git a/theories/logrel_heaplang/lib/symbol_adt.v b/theories/logrel_heaplang/lib/symbol_adt.v
index fbbe57556bb34eea8359bb3455732ef9a9b97ffe..392c7b11bbc345b04af61983d05d5006d80c9250 100644
--- a/theories/logrel_heaplang/lib/symbol_adt.v
+++ b/theories/logrel_heaplang/lib/symbol_adt.v
@@ -31,13 +31,16 @@ Section symbol_ghosts.
   Proof. apply _. Qed.
 
   Lemma counter_exclusive γ n1 n2 : counter γ n1 -∗ counter γ n2 -∗ False.
-  Proof. apply bi.wand_intro_r. by rewrite -own_op own_valid auth_validI. Qed.
+  Proof.
+    apply bi.wand_intro_r. rewrite -own_op own_valid /=. by iDestruct 1 as %[].
+  Qed.
   Global Instance symbol_persistent γ n : Persistent (symbol γ n).
   Proof. apply _. Qed.
 
   Lemma counter_alloc n : (|==> ∃ γ, counter γ n)%I.
   Proof.
-    iMod (own_alloc (● (n:mnat) ⋅ ◯ (n:mnat))) as (γ) "[Hγ Hγf]"; first done.
+    iMod (own_alloc (● (n:mnat) ⋅ ◯ (n:mnat))) as (γ) "[Hγ Hγf]";
+      first by apply auth_both_valid.
     iExists γ. by iFrame.
   Qed.
 
@@ -50,7 +53,7 @@ Section symbol_ghosts.
   Lemma symbol_obs γ s n : counter γ n -∗ symbol γ s -∗ ⌜(s < n)%nat⌝.
   Proof.
     iIntros "Hc Hs".
-    iDestruct (own_valid_2 with "Hc Hs") as %[?%mnat_included _]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "Hc Hs") as %[?%mnat_included _]%auth_both_valid.
     iPureIntro. omega.
   Qed.
 End symbol_ghosts.
diff --git a/theories/spanning_tree/mon.v b/theories/spanning_tree/mon.v
index 0ef578b577116005b00abfa4d86d0e58331bb3f8..aaaaee2a5538b8b7a409ebf10aef0fe6f796d46f 100644
--- a/theories/spanning_tree/mon.v
+++ b/theories/spanning_tree/mon.v
@@ -48,7 +48,7 @@ Section marking_definitions.
   own graph_marking_name (● (m ⋅ ({[l]} : gset loc))) ∗ is_marked l.
   Proof.
     iIntros "H". rewrite -own_op (comm _ m).
-    iMod (@own_update with "H") as "Y"; eauto.
+    iMod (own_update with "H") as "Y"; eauto.
     apply auth_update_alloc.
     setoid_replace ({[l]} : gset loc) with (({[l]} : gset loc) ⋅ ∅) at 2
       by (by rewrite right_id).
@@ -189,10 +189,10 @@ Section graph_ctx_alloc.
              ∗ own_graph 1%Qp ∅.
   Proof.
     iIntros "H1".
-    iMod (own_alloc (● (∅ : markingUR))) as (mn) "H2"; first done.
+    iMod (own_alloc (● (∅ : markingUR))) as (mn) "H2"; first by apply auth_auth_valid.
     iMod (own_alloc (● (Some (1%Qp, ∅ : Gmon) : graphUR)
                       ⋅ ◯ (Some (1%Qp, ∅ : Gmon) : graphUR))) as (gn) "H3".
-    { done. }
+    { by apply auth_both_valid. }
     iDestruct "H3" as "[H31 H32]".
     set (Ig := GraphG _ _ mn _ gn).
     iExists Ig.
@@ -279,7 +279,8 @@ Section graph.
   Lemma auth_own_graph_valid q G : own graph_name (● Some (q, G))  ⊢ ✓ G.
   Proof.
     iIntros "H". unfold own_graph.
-    by iDestruct (own_valid with "H") as %[_ [_ ?]].
+    iDestruct (own_valid with "H") as %VAL.
+    move : VAL => /auth_auth_valid [_ ?] //.
   Qed.
 
   Lemma whole_frac (G G' : Gmon):
@@ -287,10 +288,8 @@ Section graph.
   Proof.
     iIntros "[H1 H2]". rewrite /own_graph.
     iCombine "H1" "H2" as "H".
-    iDestruct (own_valid with "H") as %[H1 H2]; cbn in *.
+    iDestruct (own_valid with "H") as %[H1 H2]%auth_both_valid.
     iPureIntro.
-    specialize (H1 O).
-    apply cmra_discrete_included_iff in H1.
     apply option_included in H1; destruct H1 as [H1|H1]; [inversion H1|].
     destruct H1 as (u1 & u2 & Hu1 & Hu2 & H3);
       inversion Hu1; inversion Hu2; subst.
@@ -345,10 +344,8 @@ Section graph.
       ⊢ ⌜G = {[x := Excl w]} ⋅ (delete x G)⌝.
   Proof.
     rewrite /own_graph -?own_op. iIntros "H".
-    iDestruct (@own_valid with "H") as %[H1 H2]; simpl in *.
+    iDestruct (own_valid with "H") as %[H1 H2]%auth_both_valid.
     iPureIntro.
-    specialize (H1 O).
-    apply cmra_discrete_included_iff in H1.
     apply option_included in H1; destruct H1 as [H1|H1]; [inversion H1|].
     destruct H1 as (u1 & u2 & Hu1 & Hu2 & H1);
       inversion Hu1; inversion Hu2; subst.
@@ -399,7 +396,8 @@ Section graph.
   Proof.
     iIntros "H". unfold is_marked. rewrite -own_op.
     iDestruct (own_valid with "H") as %Hvl.
-    iPureIntro. destruct Hvl as [Hvl _]. destruct (Hvl O) as [z Hvl'].
+    move : Hvl => /auth_both_valid [[z Hvl'] _].
+    iPureIntro.
     rewrite Hvl' /= !gset_op_union !elem_of_union elem_of_singleton; tauto.
   Qed.