diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 32c9e12a613842d1e85d4e5d129d983ee8c42573..8ce1ebf6a319930490ba88e705a54790872bfbc0 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-02-16.2.bcedf1c7") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-03-09.0.f91e8eab") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v
index 3e6d7fc3d8da9765a665985620b90714703fa4e4..9d83ac5412459b9b86d2220727bc595ca62caebc 100644
--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
@@ -111,7 +111,7 @@ Section side_channel.
       wp_pures.
       by iApply "HΦ"; iRight.
     - wp_cmpxchg_fail.
-      iDestruct (own_valid_2 with "H Hγ") as %[].
+      iCombine "H Hγ" gives %[].
   Qed.
 
   (* A partial specification for take that will be useful later *)
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index 0f1605d78a4b34a071ef3417f31534ee5d0d3ada..918989ec90c7f20edeb7d4a6e3da5673622259f9 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -136,9 +136,9 @@ Section proofs.
       wp_pures.
       iApply ("HΦ" with "[HQ]"); iRight; auto.
     - wp_cmpxchg_fail.
-      iDestruct (own_valid_2 with "H Hγ") as %[].
+      iCombine "H Hγ" gives %[].
     - wp_cmpxchg_fail.
-      iDestruct (own_valid_2 with "H Hγ") as %[].
+      iCombine "H Hγ" gives %[].
   Qed.
 
   Lemma take_works γ P Q Q' o Ψ :
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index eb1428c3233d565118d7342f0b38653748d7bd5d..e3c0f949b7bef0a7cad193759183afc1104cc214 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -46,25 +46,25 @@ Lemma INIT_not_SET_RES `{saG Σ} γ q q' v :
   INIT γ q -∗ SET_RES γ q' v -∗ False.
 Proof.
   iIntros "Hs Hp".
-  iDestruct (own_valid_2 with "Hs Hp") as %[].
+  iCombine "Hs Hp" gives %[].
 Qed.
 Lemma INIT_not_FIN `{saG Σ} γ q v :
   INIT γ q -∗ FIN γ v -∗ False.
 Proof.
   iIntros "Hs Hp".
-  iDestruct (own_valid_2 with "Hs Hp") as %[].
+  iCombine "Hs Hp" gives %[].
 Qed.
 Lemma SET_RES_not_FIN `{saG Σ} γ q v v' :
   SET_RES γ q v -∗ FIN γ v' -∗ False.
 Proof.
   iIntros "Hs Hp".
-  iDestruct (own_valid_2 with "Hs Hp") as %[].
+  iCombine "Hs Hp" gives %[].
 Qed.
 Lemma SET_RES_agree `{saG Σ} (γ: gname) (q q': Qp) (v w: val) :
   SET_RES γ q v -∗ SET_RES γ q' w -∗ ⌜v = w⌝.
 Proof.
   iIntros "Hs1 Hs2".
-  iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
+  iCombine "Hs1 Hs2" gives %Hfoo.
   iPureIntro. rewrite -Cinr_op -Cinl_op -pair_op in Hfoo.
   by destruct Hfoo as [_ ?%to_agree_op_inv_L].
 Qed.
@@ -72,7 +72,7 @@ Lemma FIN_agree `{saG Σ} (γ: gname) (v w: val) :
   FIN γ v -∗ FIN γ w -∗ ⌜v = w⌝.
 Proof.
   iIntros "Hs1 Hs2".
-  iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
+  iCombine "Hs1 Hs2" gives %Hfoo.
   iPureIntro. rewrite -Cinr_op -Cinr_op in Hfoo.
   by apply to_agree_op_inv_L.
 Qed.
diff --git a/theories/hocap/contrib_bag.v b/theories/hocap/contrib_bag.v
index 5c442d5824aa647041598ef3251c404725664525..56573c38cf2eaf724bc93e0776285b9f7373553c 100644
--- a/theories/hocap/contrib_bag.v
+++ b/theories/hocap/contrib_bag.v
@@ -98,7 +98,7 @@ Section proof.
       iMod (bag_contents_update b Y with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
       rewrite /bagPart.
       iAssert (⌜X = ({[+ y +]} ⊎ Y)⌝)%I with "[Hpart HPs]" as %->.
-      { iDestruct (own_valid_2 with "HPs Hpart") as %Hfoo.
+      { iCombine "HPs Hpart" gives %Hfoo.
         apply frac_auth_agree in Hfoo. by unfold_leibniz. }
       iMod (own_update_2 with "HPs Hpart") as "Hown".
       { apply (frac_auth_update _ _ _ (({[+ y +]} ⊎ Y) ∖ {[+ y +]}) (({[+ y +]} ⊎ Y) ∖ {[+ y +]})).
@@ -117,7 +117,7 @@ Section proof.
       iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
       iAssert (⌜X = ∅⌝)%I with "[Hpart HPs]" as %->.
       { rewrite /bagPart.
-        iDestruct (own_valid_2 with "HPs Hpart") as %Hfoo.
+        iCombine "HPs Hpart" gives %Hfoo.
         apply frac_auth_agree in Hfoo. by unfold_leibniz. }
       iMod ("Hcl" with "[Hb2 HPs]") as "_".
       { iNext. iExists _; iFrame. }
diff --git a/theories/hocap/lib/oneshot.v b/theories/hocap/lib/oneshot.v
index 070e2c63553fbb6803d36d1a3c724f30760dde9e..2527c9325154d5ec62530364c3d7c184bc7181d7 100644
--- a/theories/hocap/lib/oneshot.v
+++ b/theories/hocap/lib/oneshot.v
@@ -32,7 +32,7 @@ Lemma shot_agree `{oneshotG Σ} γ (v w: val) :
   shot γ v -∗ shot γ w -∗ ⌜v = w⌝.
 Proof.
   iIntros "Hs1 Hs2".
-  iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
+  iCombine "Hs1 Hs2" gives %Hfoo.
   iPureIntro. by apply to_agree_op_inv_L.
 Qed.
 Global Instance pending_fractional `{oneshotG Σ} γ : Fractional (pending γ)%I.
diff --git a/theories/lecture_notes/ccounter.v b/theories/lecture_notes/ccounter.v
index 2761d844341e4f138e09e0af7574c8308c788b9f..aec7ca2fb67171854e0f3296f8e15f963ce9a6ad 100644
--- a/theories/lecture_notes/ccounter.v
+++ b/theories/lecture_notes/ccounter.v
@@ -101,7 +101,7 @@ Section ccounter.
     - iIntros (m) "!# [HownE HOwnfrag]".
       iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
       iDestruct (makeElem_eq with "HownE H2") as %->.
-      iDestruct (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid.
+      iCombine "H1 HOwnfrag" gives %Hleq%ccounterRA_valid.
       iMod ("HClose" with "[H1 H2]") as "_".
       { iExists _; by iFrame. }
       iFrame; iIntros "!>!%".
@@ -122,7 +122,7 @@ Section ccounter.
     - iIntros (m) "!# [HownE HOwnfrag]".
       iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
       iDestruct (makeElem_eq with "HownE H2") as %->.
-      iDestruct (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid_full; simplify_eq.
+      iCombine "H1 HOwnfrag" gives %Hleq%ccounterRA_valid_full; simplify_eq.
       iMod ("HClose" with "[H1 H2]") as "_".
       { iExists _; by iFrame. }
       iFrame; by iIntros "!>!%".
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index 208e2ad6347295a6e26f9374909a3dfb5c91965a..1affbc1b57df9e668679be6906f219731ad16409 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -295,7 +295,7 @@ Section monotone_counter.
     wp_load.
     (* NOTE: We use the validity property of the RA we have constructed. From the fact that we own 
              ◯ n and ● m to conclude that n ≤ m. *)
-    iDestruct (own_valid_2 with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag. 
+    iCombine "HOwnAuth HOwnFrag" gives %H%mcounterRA_valid_auth_frag. 
     iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
     { iNext; iExists m; iFrame. }
     iModIntro.
@@ -653,7 +653,7 @@ Section ccounter.
   Proof.
     iIntros (Φ) "[Hown #Hinv] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hpt]" "Hclose". wp_load.
-    iDestruct (own_valid_2 with "Hγ Hown") as % ?%ccounterRA_valid. (* We use the validity property of our RA. *)
+    iCombine "Hγ Hown" gives % ?%ccounterRA_valid. (* We use the validity property of our RA. *)
     iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists c; by iFrame|].
     iApply ("HΦ" with "[-]"); rewrite /is_ccounter; eauto.
   Qed.
@@ -664,7 +664,7 @@ Section ccounter.
   Proof.
     iIntros (Φ) "[Hown #Hinv] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hpt]" "Hclose". wp_load.
-    iDestruct (own_valid_2 with "Hγ Hown") as % <-%ccounterRA_valid_full. (* We use the validity property of our RA. *)
+    iCombine "Hγ Hown" gives % <-%ccounterRA_valid_full. (* We use the validity property of our RA. *)
     iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists n; by iFrame|].
     iApply "HΦ"; iModIntro. iFrame "Hown #"; done.
   Qed.
diff --git a/theories/lecture_notes/lock.v b/theories/lecture_notes/lock.v
index 4994a2e5dcc895038655f42873686e7d3f247b79..b1bc4d521bc4b6e32f9b67b9409db21ddf6e1f12 100644
--- a/theories/lecture_notes/lock.v
+++ b/theories/lecture_notes/lock.v
@@ -122,7 +122,7 @@ Section lock_spec.
     iDestruct "Hi" as (ℓ ->) "Hinv".
     wp_lam.
     iInv (lockN #ℓ) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
-    - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
+    - iCombine "Hld Ht" gives %Hv. done.
     - wp_store.
       iMod ("Hcl" with "[-Hcont]") as "_"; first by iNext; iLeft; iFrame.
       iApply "Hcont".
diff --git a/theories/lecture_notes/lock_unary_spec.v b/theories/lecture_notes/lock_unary_spec.v
index 7ab0883f8102ce9ed33a8bc7cc1788c752afb96d..e122dd3667beee5a2b7fa07b4dc0cd768b921470 100644
--- a/theories/lecture_notes/lock_unary_spec.v
+++ b/theories/lecture_notes/lock_unary_spec.v
@@ -135,7 +135,7 @@ Section lock_spec.
     iIntros (HE φ) "(#Hi & Hld & HP) Hcont"; rewrite /release.
     wp_lam.
     iInv (lockN l) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
-    - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
+    - iCombine "Hld Ht" gives %Hv. done.
     - wp_store.
       iMod ("Hcl" with "[-Hcont]") as "_"; first by iNext; iLeft; iFrame.
       iApply "Hcont".
@@ -194,7 +194,7 @@ Section lock_spec.
     iIntros (HE) "(#Hi & Hld & HP)"; rewrite /release.
     wp_lam.
     iInv (lockN l) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
-    - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
+    - iCombine "Hld Ht" gives %Hv. done.
     - wp_store.
       iMod ("Hcl" with "[-]") as "_"; first by iNext; iLeft; iFrame.
       done.
diff --git a/theories/lecture_notes/modular_incr.v b/theories/lecture_notes/modular_incr.v
index 9edae971a7cdda6c785f133926187f7129e8b80e..8ff6a39bceb7b372818db7047e88bb2842dabda9 100644
--- a/theories/lecture_notes/modular_incr.v
+++ b/theories/lecture_notes/modular_incr.v
@@ -75,7 +75,7 @@ Section cnt_model.
     γ ⤇[p] n -∗ γ ⤇[q] m -∗ ⌜n = m⌝.
   Proof.
     iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %HValid.
+    iCombine "H1 H2" gives %HValid.
     destruct HValid as [_ H2].
     iIntros "!%"; by apply to_agree_op_inv_L.
   Qed.
diff --git a/theories/locks/array_based_queuing_lock/abql.v b/theories/locks/array_based_queuing_lock/abql.v
index ba86dd4d88016051249f33ef1dfb0342d519ba52..a0af45714b9c711e19b3664361b07e77c30cc100 100644
--- a/theories/locks/array_based_queuing_lock/abql.v
+++ b/theories/locks/array_based_queuing_lock/abql.v
@@ -282,7 +282,7 @@ Section proof.
   Lemma locked_exclusive (γ κ : gname) o o' : locked γ κ o -∗ locked γ κ o' -∗ False.
   Proof.
     iIntros "[H1 _] [H2 _]".
-    iDestruct (own_valid_2 with "H1 H2") as %[[] _]%auth_frag_op_valid_1.
+    iCombine "H1 H2" gives %[[] _]%auth_frag_op_valid_1.
   Qed.
 
   (* Only one thread can know the exact value of `o`. *)
@@ -290,7 +290,7 @@ Section proof.
     own γ (◯ (Excl' o, GSet ∅)) -∗ own γ (◯ (Excl' o', GSet ∅)) -∗ False.
   Proof.
     iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[[]]%auth_frag_op_valid_1.
+    iCombine "H1 H2" gives %[[]]%auth_frag_op_valid_1.
   Qed.
 
   (* Lemmas about both, left, and right. *)
@@ -317,7 +317,7 @@ Section proof.
         -∗ ⌜o ≤ x < o + i⌝ ∗ own γ (◯ (ε, GSet {[ x ]})) ∗ own γ (● (Excl' o, GSet (set_seq o i))).
   Proof.
     iIntros "P O".
-    iDestruct (own_valid_2 with "O P") as %[[_ xIncl%gset_disj_included]%prod_included Hv]%auth_both_valid_discrete.
+    iCombine "O P" gives %[[_ xIncl%gset_disj_included]%prod_included Hv]%auth_both_valid_discrete.
     iFrame. iPureIntro.
     apply elem_of_subseteq_singleton, elem_of_set_seq in xIncl.
     lia.
@@ -328,7 +328,7 @@ Section proof.
       -∗ ⌜0 < i⌝ ∗ own γ (◯ (ε, GSet {[ o ]})) ∗ own γ (● (Excl' o, GSet (set_seq o i))).
   Proof.
     iIntros "P O".
-    iDestruct (own_valid_2 with "O P") as %HV%auth_both_valid_discrete.
+    iCombine "O P" gives %HV%auth_both_valid_discrete.
     iFrame. iPureIntro.
     destruct HV as [[_ H%gset_disj_included]%prod_included _].
     apply elem_of_subseteq_singleton, set_seq_len_pos in H.
@@ -542,7 +542,7 @@ Section proof.
     wp_bind (_ <- _)%E.
     iInv N as (o' i xs) "(>%lenEq & >nextPts & arrPts & >Invs & >Auth & Part)" "Close".
     (* We want to show that o and o' are equal. We know this from the loked γ o ghost state. *)
-    iDestruct (own_valid_2 with "Auth Locked") as
+    iCombine "Auth Locked" gives
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
     rewrite rem_mod_eq //.
     iApply (array_store with "[arrPts]").
@@ -569,7 +569,7 @@ Section proof.
     * iDestruct (know_o_exclusive with "Locked Locked'") as "[]".
     (* This is the case where the lock is clopen, that is, the actual state
        of the lock. *)
-    * iDestruct (own_valid_2 with "Auth Locked") as
+    * iCombine "Auth Locked" gives
           %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
       rewrite rem_mod_eq //.
       iApply (wp_store_offset with "arrPts").
diff --git a/theories/locks/freeable_lock/freeable_logatom_lock.v b/theories/locks/freeable_lock/freeable_logatom_lock.v
index 6ac6b470fc2c2f55bbdd4074045950eb471cf602..e650008a3b34f5059f1e0513d94c133358eeb3cd 100644
--- a/theories/locks/freeable_lock/freeable_logatom_lock.v
+++ b/theories/locks/freeable_lock/freeable_logatom_lock.v
@@ -85,7 +85,7 @@ Section tada.
     tada_lock_state γ s1 -∗ ghost_var γ.(tada_lock_name_state) (3/4) s2 -∗ False.
   Proof.
     iIntros "[Hvar1 _] Hvar2".
-    iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[Hval _].
+    iCombine "Hvar1 Hvar2" gives %[Hval _].
     exfalso. done.
   Qed.
   Lemma tada_lock_state_exclusive γ s1 s2 :
diff --git a/theories/locks/freeable_lock/freeable_spin_lock.v b/theories/locks/freeable_lock/freeable_spin_lock.v
index 83237ecabf47d80524b5a142c187471f6043e563..b59be5831feec03fd3393d9e94a0759365e52304 100644
--- a/theories/locks/freeable_lock/freeable_spin_lock.v
+++ b/theories/locks/freeable_lock/freeable_spin_lock.v
@@ -49,7 +49,7 @@ Section proof.
     own γ.(spin_lock_name_own) q.
 
   Lemma locked_exclusive (γ : spin_lock_name) : locked γ -∗ locked γ -∗ False.
-  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
+  Proof. iIntros "H1 H2". by iCombine "H1 H2" gives %?. Qed.
 
   Lemma own_lock_valid (γ : spin_lock_name) q :
     own_lock γ q -∗ ⌜q ≤ 1⌝%Qp.
@@ -105,7 +105,7 @@ Section proof.
   Proof.
     iIntros (Φ) "[#Hl Hown] HΦ". iDestruct "Hl" as (l ->) "#Hinv".
     wp_rec. wp_bind (CmpXchg _ _ _). iInv N as "[Hlock|>[_ Hcancel]]"; last first.
-    { rewrite /own_lock. iDestruct (own_valid_2 with "Hown Hcancel") as %Hc.
+    { rewrite /own_lock. iCombine "Hown Hcancel" gives %Hc.
       rewrite frac_op frac_valid in Hc. exfalso. eapply Qp.not_add_le_r. done. }
     iDestruct "Hlock" as ([]) "[Hl HR]".
     - wp_cmpxchg_fail. iModIntro. iSplitL "Hl"; first (iNext; iLeft; iExists true; eauto).
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index f4682c4c12ba393c9457f4677d914cb3e568a178..6afcd992d6a942102e1fd8af9705c9e131dc3103 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -220,7 +220,7 @@ Section conditional_counter.
     counter_content γs c1 -∗ counter_content γs c2 -∗ False.
   Proof.
     iIntros "Hb1 Hb2".
-    iDestruct (own_valid_2 with "Hb1 Hb2") as %?%auth_frag_op_valid_1.
+    iCombine "Hb1 Hb2" gives %?%auth_frag_op_valid_1.
     done.
   Qed.
 
@@ -243,10 +243,10 @@ Section conditional_counter.
     iInv stateN as (vs) "(Hp & [NotDone | Done])".
     * (* Moved back to NotDone: contradiction. *)
       iDestruct "NotDone" as "(>Hs' & _ & _)".
-      iDestruct (own_valid_2 with "Hs Hs'") as %?. contradiction.
+      iCombine "Hs Hs'" gives %?. contradiction.
     * iDestruct "Done" as "(_ & QT & Hghost)".
       iDestruct "QT" as "[Q | >T]"; last first.
-      { iDestruct (own_valid_2 with "Ht T") as %Contra.
+      { iCombine "Ht T" gives %Contra.
           by inversion Contra. }
       iSplitR "Q"; last done. iIntros "!> !>". unfold state_inv.
       iExists _. iFrame "Hp". iRight.
@@ -273,7 +273,7 @@ Section conditional_counter.
          as token for that transition. *)
       iDestruct "Done" as "(_ & _ & Hlghost & _)".
       iDestruct "Hlghost" as (v') ">Hlghost".
-        by iDestruct (mapsto_valid_2 with "Hl_ghost Hlghost") as %[??].
+        by iCombine "Hl_ghost Hlghost" gives %[??].
     }
     iDestruct "NotDone" as "(>Hs & >Hc' & [Pending | Accepted])".
     { (* We also cannot be [Pending] any more we have [own γ_n] showing that this
@@ -408,12 +408,12 @@ Section conditional_counter.
         iDestruct "Accepted" as "[>Hl_ghost_inv _]".
         iDestruct "Hl_ghost_inv" as (v) "Hlghost".
         iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
-        by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %[??].
+        by iCombine "Hlghost Hl_ghost'" gives %[??].
       + (* Done: contradiction *)
         iDestruct "Done" as "[QT >[Hlghost _]]".
         iDestruct "Hlghost" as (v) "Hlghost".
         iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
-        by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %[??].
+        by iCombine "Hlghost Hl_ghost'" gives %[??].
     - (* we are the failing thread. exploit that [f] is a GC location. *)
       iMod (inv_mapsto_acc with "GC isGC") as (b) "(_ & H↦ & Hclose)"; first solve_ndisj.
       wp_load.
diff --git a/theories/logatom/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v
index 97713ff45f9d5be36b5b1cf02f94d86e037db038..220e3f971a92accdc3f7e81ffde64a5ac1a14e22 100644
--- a/theories/logatom/counter_with_backup/counter_proof.v
+++ b/theories/logatom/counter_with_backup/counter_proof.v
@@ -425,7 +425,7 @@ Section counter_proof.
       iExists Ψ. rewrite bool_decide_eq_false_2 //. iFrame.
     - iDestruct "Done" as "[_ Htok]".
       (* contradictory *)
-      iDestruct (own_valid_2 with "Hex Htok") as %[].
+      iCombine "Hex Htok" gives %[].
   Qed.
 
   (** We obtain the post condition of the AU for [put] after it has been executed,
@@ -466,7 +466,7 @@ Section counter_proof.
       rewrite bool_decide_eq_false_2 //.
       iFrame.
     - iDestruct "Done" as "[_ Htok]".
-      iDestruct (own_valid_2 with "Hex Htok") as %[].
+      iCombine "Hex Htok" gives %[].
   Qed.
 
   (** ** Proving the actual specs for the counter operations *)
@@ -653,7 +653,7 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros ???? [γ_cnt γ_ex] ??. iIntros "[_ H1] [_ H2]".
-  iDestruct (own_valid_2 with "H1 H2") as %[].
+  iCombine "H1 H2" gives %[].
 Qed.
 
 Global Typeclasses Opaque value is_counter.
diff --git a/theories/logatom/elimination_stack/hocap_spec.v b/theories/logatom/elimination_stack/hocap_spec.v
index ed453a2724cb513d96cb8fc25ac544ebf0bd17e4..885c1d77d953fa2707399962bcf9e9f443d6669a 100644
--- a/theories/logatom/elimination_stack/hocap_spec.v
+++ b/theories/logatom/elimination_stack/hocap_spec.v
@@ -350,14 +350,14 @@ Section hocap_pred_auth.
        hocap_auth.pop_spec := hocap_auth_pop |}.
   Next Obligation.
     iIntros (???) "Hf1 Hf2".
-    iDestruct (own_valid_2 with "Hf1 Hf2") as %[]%auth_frag_op_valid_1.
+    iCombine "Hf1 Hf2" gives %[]%auth_frag_op_valid_1.
   Qed.
   Next Obligation.
     iIntros (???) "Ha1 Ha2".
-    iDestruct (own_valid_2 with "Ha1 Ha2") as %[]%auth_auth_op_valid.
+    iCombine "Ha1 Ha2" gives %[]%auth_auth_op_valid.
   Qed.
   Next Obligation.
-    iIntros (???) "Hf Ha". iDestruct (own_valid_2 with "Ha Hf") as
+    iIntros (???) "Hf Ha". iCombine "Ha Hf" gives
       %[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete. done.
   Qed.
   Next Obligation.
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index 28bdeae83d7fde9a0584786e7059209c32886956..146a6c70f67056d11e008b77538ec4268e7468ac 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -96,7 +96,7 @@ Section stack.
     stack_content γs l1 -∗ stack_content γs l2 -∗ False.
   Proof.
     iIntros "Hl1 Hl2".
-    iDestruct (own_valid_2 with "Hl1 Hl2") as %[]%auth_frag_op_valid_1.
+    iCombine "Hl1 Hl2" gives %[]%auth_frag_op_valid_1.
   Qed.
 
   Definition stack_elem_to_val (stack_rep : option loc) : val :=
@@ -210,7 +210,7 @@ Section stack.
     - (* The CAS succeeded. Update everything accordingly. *)
       iMod "AU" as (l') "[Hl' [_ Hclose]]".
       iMod (mapsto_persist with "Hhead_new") as "#Hhead_new".
-      iDestruct (own_valid_2 with "Hs● Hl'") as
+      iCombine "Hs● Hl'" gives
         %[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
       iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
       { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
@@ -255,14 +255,14 @@ Section stack.
         wp_if. iApply ("IH" with "AU").
       + (* Offer revoked by someone else? Impossible! *)
         iDestruct "Hst" as ">Hst".
-        iDestruct (own_valid_2 with "Htok Hst") as %[].
+        iCombine "Htok Hst" gives %[].
       + (* Offer got accepted by someone, awesome! We are done. *)
         iModIntro. iSplitR "Hst".
         { iNext. iExists OfferAcked. iFrame. }
         wp_if. by iApply "Hst".
       + (* Offer got acked by someone else? Impossible! *)
         iDestruct "Hst" as ">Hst".
-        iDestruct (own_valid_2 with "Htok Hst") as %[].
+        iCombine "Htok Hst" gives %[].
   Qed.
 
   Lemma pop_spec γs (s : val) :
@@ -284,7 +284,7 @@ Section stack.
       prove that. *)
       iDestruct "Hlist" as ">%". subst stack_rep.
       iMod "AU" as (l') "[Hl' [_ Hclose]]".
-      iDestruct (own_valid_2 with "Hs● Hl'") as
+      iCombine "Hs● Hl'" gives
         %[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
       iMod ("Hclose" with "Hl'") as "HΦ".
       iSplitR "HΦ"; first by eauto 10 with iFrame.
@@ -306,7 +306,7 @@ Section stack.
       + (* CAS succeeded! It must still be the same head element in the list,
         and we are done. *)
         iMod "AU" as (l') "[Hl' [_ Hclose]]".
-        iDestruct (own_valid_2 with "Hs● Hl'") as
+        iCombine "Hs● Hl'" gives
           %[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
         destruct l as [|v' l]; simpl.
         { (* Contradiction. *) iDestruct "Hlist" as ">%". done. }
@@ -346,13 +346,13 @@ Section stack.
         iMod (lc_fupd_elim_later with "Hlc Hoff") as "AUoff".
         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
+        iCombine "Hs● Hl'" gives
           %[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
         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
+        iCombine "Hs● Hl'" gives
           %[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
         iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
         { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index fa6f4eaa68fa107442bd190a43b8bf82e663675f..0aa9e761b2a410054aeb6ad8b3d4b60b3fb12a27 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -180,7 +180,7 @@ Lemma hwq_cont_exclusive γe elts1 elts2 :
   hwq_cont γe elts1 -∗ hwq_cont γe elts2 -∗ False.
 Proof.
   iIntros "H1 H2".
-  by iDestruct (own_valid_2 with "H1 H2") as %?%auth_frag_op_valid_1.
+  by iCombine "H1 H2" gives %?%auth_frag_op_valid_1.
 Qed.
 
 (** Operations for the CMRA used to show that back only increases. *)
@@ -258,12 +258,12 @@ Proof. apply own_update. by apply cmra_update_exclusive. Qed.
 
 Lemma contra_not_no_contra i1 i2 γc :
   no_contra γc -∗ contra γc i1 i2 -∗ False.
-Proof. iIntros "HnoC HC". iDestruct (own_valid_2 with "HnoC HC") as %[]. Qed.
+Proof. iIntros "HnoC HC". iCombine "HnoC HC" gives %[]. Qed.
 
 Lemma contra_agree i1 i2 i1' i2' γc :
   contra γc i1 i2 -∗ contra γc i1' i2' -∗ ⌜i1' = i1 ∧ i2' = i2⌝.
 Proof.
-  iIntros "HC HC'". iDestruct (own_valid_2 with "HC HC'") as %H.
+  iIntros "HC HC'". iCombine "HC HC'" gives %H.
   iPureIntro. apply to_agree_op_inv_L in H. by inversion H.
 Qed.
 
@@ -436,7 +436,7 @@ Lemma use_val_wit γs slots i l :
   slot_val_wit γs i l -∗
   ⌜val_of <$> slots !! i = Some l⌝.
 Proof.
-  iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+  iIntros "H● Hwit". iCombine "H● Hwit" gives %H.
   iPureIntro. apply auth_both_valid_discrete in H as [H%singleton_included_l _].
   destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
   destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
@@ -469,7 +469,7 @@ Lemma use_name_tok γs slots i γ :
   slot_name_tok γs i γ -∗
   ⌜name_of <$> slots !! i = Some (Some γ)⌝.
 Proof.
-  iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+  iIntros "H● Hwit". iCombine "H● Hwit" gives %H.
   iPureIntro. apply auth_both_valid_discrete in H as [H%singleton_included_l _].
   destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
   destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
@@ -538,7 +538,7 @@ Lemma use_committed_wit γs slots i :
   slot_committed_wit γs i -∗
   ⌜was_committed <$> slots !! i = Some true⌝.
 Proof.
-  iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+  iIntros "H● Hwit". iCombine "H● Hwit" gives %H.
   iPureIntro. apply auth_both_valid_discrete in H as [H%singleton_included_l _].
   destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
   destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
@@ -564,7 +564,7 @@ Lemma use_written_wit γs slots i :
   slot_written_wit γs i -∗
   ⌜was_written <$> slots !! i = Some true⌝.
 Proof.
-  iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+  iIntros "H● Hwit". iCombine "H● Hwit" gives %H.
   iPureIntro. apply auth_both_valid_discrete in H as [H%singleton_included_l _].
   destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
   destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index b33a7e9259367a49fd630816dac58cdc0a08438d..00dc678c95f149be32df009228d11cfab2adf24f 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -334,7 +334,7 @@ Section rdcss.
     iDestruct "Hn1" as (γ_1) "[#Meta1 Hn1]".
     iDestruct "Hn2" as (γ_2) "[#Meta2 Hn2]".
     iDestruct (meta_agree with "Meta1 Meta2") as %->.
-    by iDestruct (own_valid_2 with "Hn1 Hn2") as %?%auth_frag_op_valid_1.
+    by iCombine "Hn1 Hn2" gives %?%auth_frag_op_valid_1.
   Qed.
 
   (** A few more helper lemmas that will come up later *)
@@ -350,10 +350,10 @@ Section rdcss.
     iInv descrN as (vs) "(Hp & [NotDone | Done])".
     * (* Moved back to NotDone: contradiction. *)
       iDestruct "NotDone" as "(>Hs' & _ & _)".
-      iDestruct (own_valid_2 with "Hs Hs'") as %?. contradiction.
+      iCombine "Hs Hs'" gives %?. contradiction.
     * iDestruct "Done" as "(_ & QT & Hrest)".
       iDestruct "QT" as "[Qn | >T]"; last first.
-      { iDestruct (own_valid_2 with "Ht T") as %Contra.
+      { iCombine "Ht T" gives %Contra.
           by inversion Contra. }
       iSplitR "Qn"; last done. iIntros "!> !>". unfold descr_inv.
       iExists _. iFrame "Hp". iRight.
@@ -378,12 +378,12 @@ Section rdcss.
     { (* We cannot be [done] yet, as we own the [γ_a] token that serves
          as token for that transition. *)
       iDestruct "Done" as "(_ & _ & _ & _ & >Token_a')".
-      by iDestruct (own_valid_2 with "Token_a Token_a'") as %?.
+      by iCombine "Token_a Token_a'" gives %?.
     }
     iDestruct "NotDone" as "(>Hs & >Hln' & [Pending | Accepted])".
     { (* We also cannot be [Pending] any more because we own the [γ_a] token. *)
       iDestruct "Pending" as "[_ >(_ & _ & Token_a')]".
-      by iDestruct (own_valid_2 with "Token_a Token_a'") as %?.
+      by iCombine "Token_a Token_a'" gives %?.
     }
     (* So, we are [Accepted]. Now we can show that (InjRV l_descr) = (state_to_val s), because
        while a [descr] protocol is not [done], it owns enough of
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 07f8cf6979ff0c2940a8ef96212d2a56987d9bef..02f0625ae6d2699ecf89e8d68483006b42a23240 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -117,7 +117,7 @@ Section atomic_snapshot.
     snapshot_content γs a1 -∗ snapshot_content γs a2 -∗ False.
   Proof.
     iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[]%auth_frag_op_valid_1.
+    iCombine "H1 H2" gives %[]%auth_frag_op_valid_1.
   Qed.
 
   Definition new_timestamp t v : gmap Z val := {[ t := v ]}.
@@ -165,7 +165,7 @@ Section atomic_snapshot.
     own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) -∗ ⌜m = n⌝.
   Proof.
     iIntros "Hγ● Hγ◯".
-    iDestruct (own_valid_2 with "Hγ● Hγ◯") as
+    iCombine "Hγ● Hγ◯" gives
         %[H%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
     done.
   Qed.
@@ -196,7 +196,7 @@ Section atomic_snapshot.
     ⌜∀ t x, T2 !! t = Some x → T1 !! t = Some x⌝.
   Proof.
     iIntros "[Hγ⚫ Hγ◯]".
-    iDestruct (own_valid_2 with "Hγ⚫ Hγ◯") as
+    iCombine "Hγ⚫ Hγ◯" gives
         %[H Hv]%auth_both_valid_discrete. 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.
diff --git a/theories/logrel/F_mu_ref_conc/binary/logrel.v b/theories/logrel/F_mu_ref_conc/binary/logrel.v
index 83746b9dc6ca37d92ae2c667465844e10f6ec70d..3b25de1d7bbb41933c5a814a80e88ecb425e83ff 100644
--- a/theories/logrel/F_mu_ref_conc/binary/logrel.v
+++ b/theories/logrel/F_mu_ref_conc/binary/logrel.v
@@ -257,26 +257,26 @@ Section logrel.
       + destruct (decide (l2 = l)); simplify_eq.
         * destruct (decide (l2' = l')); simplify_eq; first by iFrame.
           iInv (logN.@(l, l2')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
-          iDestruct (mapsto_valid_2 with "Hl Hlx") as %[? ?]; done.
+          iCombine "Hl Hlx" gives %[? ?]; done.
         * destruct (decide (l2' = l')); simplify_eq; last first.
           { iModIntro; iFrame; iPureIntro; intuition simplify_eq. }
           iInv (logN.@(l2, l')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
-          iDestruct (mapstoS_valid_2 with "Hl' Hlx'") as %?; done.
+          iCombine "Hl' Hlx'" gives %[??]; done.
       + iInv (logN.@(l, l1')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
-          iDestruct (mapsto_valid_2 with "Hl Hlx") as %[? ?]; done.
+          iCombine "Hl Hlx" gives %[? ?]; done.
     - destruct (decide (l1 = l2)); simplify_eq.
       + destruct (decide (l1' = l2')); simplify_eq; first by iFrame.
         iInv (logN.@(l2, l1')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
         iInv (logN.@(l2, l2')) as ([w w']) "(>Hly & >Hly' & Hww) /=" "Hclose'".
-        iDestruct (mapsto_valid_2 with "Hly Hlx") as %[? ?]; done.
+        iCombine "Hly Hlx" gives %[? ?]; done.
       + destruct (decide (l1' = l2')); simplify_eq; last first.
         { iModIntro; iFrame; iPureIntro; intuition simplify_eq. }
         destruct (decide (l2' = l')); simplify_eq.
         * iInv (logN.@(l1, l')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
-          iDestruct (mapstoS_valid_2 with "Hl' Hlx'") as %?; done.
+          iCombine "Hl' Hlx'" gives %[??]; done.
         * iInv (logN.@(l1, l2')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
           iInv (logN.@(l2, l2')) as ([w w']) "(>Hly & >Hly' & Hww) /=" "Hclose'".
-          iDestruct (mapstoS_valid_2 with "Hly' Hlx'") as %?; done.
+          iCombine "Hly' Hlx'" gives %[??]; done.
   Qed.
 
 End logrel.
diff --git a/theories/logrel/F_mu_ref_conc/binary/rules.v b/theories/logrel/F_mu_ref_conc/binary/rules.v
index 616ab06bcb68251c72f80e77a5471ba8fdb5669e..b5a9e31bc82c2f988843b1b9827b7d2cb1d75823 100644
--- a/theories/logrel/F_mu_ref_conc/binary/rules.v
+++ b/theories/logrel/F_mu_ref_conc/binary/rules.v
@@ -189,6 +189,14 @@ Section cfg.
     by iApply (mapstoS_valid l _ v2).
   Qed.
 
+  Global Instance mapstoS_combine_sep_gives l dq1 dq2 v1 v2 :
+    CombineSepGives (l ↦ₛ{dq1} v1) (l ↦ₛ{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
+  Proof.
+    rewrite /CombineSepGives. iIntros "[H1 H2]". iSplit.
+    - iDestruct (mapstoS_valid_2 with "H1 H2") as %?; auto.
+    - iDestruct (mapstoS_agree with "H1 H2") as %?; auto.
+  Qed.
+
   Lemma step_insert K tp j e σ κ e' σ' efs :
     tp !! j = Some (fill K e) → head_step e σ κ e' σ' efs →
     erased_step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
diff --git a/theories/logrel/F_mu_ref_conc/binary/soundness.v b/theories/logrel/F_mu_ref_conc/binary/soundness.v
index 91c9fd8c791ec6c031307ecc31c3759161a5159a..d17fc858e560087fd55b1a808d002d67de8afc3e 100644
--- a/theories/logrel/F_mu_ref_conc/binary/soundness.v
+++ b/theories/logrel/F_mu_ref_conc/binary/soundness.v
@@ -44,7 +44,7 @@ Proof.
   - iModIntro. iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
     iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
     rewrite /tpool_mapsto /=.
-    iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
+    iCombine "Hown Hj" gives %Hvalid.
     move: Hvalid=> /auth_both_valid_discrete
       [/prod_included [/tpool_singleton_included Hv2 _] _].
     destruct tp as [|? tp']; simplify_eq/=.
diff --git a/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v b/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
index aa06206f38261627bdda3d3e6937691df8c5a61c..11439b0f73a0d5b999e8a30821f71eb63858dc97 100644
--- a/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
+++ b/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
@@ -47,7 +47,7 @@ Section symbol_nat_sem_typ.
   Proof.
     iIntros "Hmt Htk".
     rewrite /Max_token /Token; simpl.
-    by iDestruct (own_valid_2 with "Hmt Htk") as
+    by iCombine "Hmt Htk" gives
         %[?%max_nat_included _]%auth_both_valid_discrete.
   Qed.
 
diff --git a/theories/proph/eager_coin.v b/theories/proph/eager_coin.v
index 91958dc2e6bcf08d0f6da14580c7ff79720d568b..572a49a03ffbf54407deb5e434fd9368ce3853d3 100644
--- a/theories/proph/eager_coin.v
+++ b/theories/proph/eager_coin.v
@@ -26,7 +26,7 @@ Section proof.
     iDestruct "H1" as (l1) "[% Hl1]".
     iDestruct "H2" as (l2) "[% Hl2]".
     simplify_eq.
-    by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
+    by iCombine "Hl1 Hl2" gives %[??].
   Qed.
 
   Lemma new_eager_coin_spec :
diff --git a/theories/proph/lazy_coin_one_shot.v b/theories/proph/lazy_coin_one_shot.v
index ed9c68e1c79e30b070cb2f5b3228403a83f32c97..b6015f3073d977470fc4cb63f0f4981efbfa3f43 100644
--- a/theories/proph/lazy_coin_one_shot.v
+++ b/theories/proph/lazy_coin_one_shot.v
@@ -48,7 +48,7 @@ Section proof.
     simplify_eq.
     iDestruct "H1" as "[Hc1 | [Hc1 _]]";
     iDestruct "H2" as "[Hc2 | [Hc2 _]]";
-    by iDestruct (mapsto_valid_2 with "Hc1 Hc2") as %[??].
+    by iCombine "Hc1 Hc2" gives %[??].
   Qed.
 
   Lemma new_lazy_coin_spec :
diff --git a/theories/proph/lazy_coin_one_shot_typed.v b/theories/proph/lazy_coin_one_shot_typed.v
index 2cc2d5e1375384d12cdf4bcdf7935d4b6af83c3f..9abef6bee62d438859bb2d1ae87c795d001d5886 100644
--- a/theories/proph/lazy_coin_one_shot_typed.v
+++ b/theories/proph/lazy_coin_one_shot_typed.v
@@ -40,7 +40,7 @@ Section proof.
     simplify_eq.
     iDestruct "H1" as "[Hc1 | [Hc1 _]]";
     iDestruct "H2" as "[Hc2 | [Hc2 _]]";
-    by iDestruct (mapsto_valid_2 with "Hc1 Hc2") as %[??].
+    by iCombine "Hc1 Hc2" gives %[??].
   Qed.
 
   Lemma new_lazy_coin_spec :