diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index ecbbd0604faa3cfc90d6f624bdf2eefdebf7800b..22855277e444645e250d027c46713429bdbe2f41 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2023-03-07.1.7e127436") | (= "dev") }
+  "coq-iris"  { (= "dev.2023-03-10.0.45e5a052") }
   "coq-orc11" {= version}
 ]
 
diff --git a/gpfsl-examples/circ_buff/proof_gps.v b/gpfsl-examples/circ_buff/proof_gps.v
index 1c4232a42cd5871b31f18e0af0ebdcc272a53d31..e225849acea9c30a0ec1a1f3983f16770c4c7a00 100644
--- a/gpfsl-examples/circ_buff/proof_gps.v
+++ b/gpfsl-examples/circ_buff/proof_gps.v
@@ -91,7 +91,7 @@ Context `{!noprolG Σ, cirbG: !cbG Σ, !atomicG Σ}.
 Lemma pTok_exclusive γ i: pTok γ i ∗ pTok γ i ⊢ False.
 Proof.
   iIntros "[T1 T2]".
-  iDestruct (own_valid_2 with "T1 T2") as %[Valid _].
+  iCombine "T1 T2" gives %[Valid _].
   exfalso. simpl in Valid.
   rewrite -> coPset_disj_valid_op, disjoint_singleton_l in Valid.
   by apply Valid, elem_of_singleton.
@@ -100,7 +100,7 @@ Qed.
 Lemma cTok_exclusive γ i: cTok γ i ∗ cTok γ i ⊢ False.
 Proof.
   iIntros "[T1 T2]".
-  iDestruct (own_valid_2 with "T1 T2") as %[_ Valid].
+  iCombine "T1 T2" gives %[_ Valid].
   exfalso. simpl in Valid.
   rewrite ->coPset_disj_valid_op, disjoint_singleton_l in Valid.
   by apply Valid, elem_of_singleton.
diff --git a/gpfsl-examples/exchanger/proof_graph_piggyback.v b/gpfsl-examples/exchanger/proof_graph_piggyback.v
index 77c408453f8c5498b3466fc68f9e5b0fc00f4b26..1755d411e96bf55677f3d7924fd46c4f9f12ece2 100644
--- a/gpfsl-examples/exchanger/proof_graph_piggyback.v
+++ b/gpfsl-examples/exchanger/proof_graph_piggyback.v
@@ -611,7 +611,7 @@ Lemma LTM_master_snap_included γ T T' :
   LTM_master γ T -∗ LTM_snap γ T' -∗ ⌜T' ⊆ T⌝.
 Proof.
   iIntros "o1 o2".
-  iDestruct (own_valid_2 with "o1 o2") as %[INCL ?]%auth_both_valid_discrete.
+  iCombine "o1 o2" gives %[INCL ?]%auth_both_valid_discrete.
   iPureIntro. by move : INCL => /= /to_agreeM_included.
 Qed.
 Lemma LTM_master_ssnap_lookup γ M l i :
diff --git a/gpfsl-examples/exchanger/proof_mp_client.v b/gpfsl-examples/exchanger/proof_mp_client.v
index ef0af0e3e910d2dfa5dae249a62e1204e0a34852..58d6c26d4b1915f01dc4445104c8c09506a4e753 100644
--- a/gpfsl-examples/exchanger/proof_mp_client.v
+++ b/gpfsl-examples/exchanger/proof_mp_client.v
@@ -110,7 +110,7 @@ Section ex.
       iMod "Close2" as "_".
       (* Update the ghost state *)
       iDestruct "Hown" as (b1 b2) "[[>Hown1 Hown2] >[%Hsize _]]".
-      iDestruct (own_valid_2 with "Hown1 Tokγ11") as %->%excl_auth_agree_L.
+      iCombine "Hown1 Tokγ11" gives %->%excl_auth_agree_L.
       iMod (own_update_2 with "Hown1 Tokγ11") as "[Hown1 Tokγ11]".
       { apply (excl_auth_update _ _ true). }
       (* Close the client invariant *)
@@ -146,7 +146,7 @@ Section ex.
       (* Close other masks *)
       iMod "Close2" as "_".
       iDestruct "Hown" as (b1 b2) "[[>Hown1 >Hown2] >[%Hsize %Eqb1]]".
-      iDestruct (own_valid_2 with "Hown2 Tokγ21") as %->%excl_auth_agree_L.
+      iCombine "Hown2 Tokγ21" gives %->%excl_auth_agree_L.
       iMod (own_update_2 with "Hown2 Tokγ21") as "[Hown2 Tokγ21]".
       { apply (excl_auth_update _ _ true). }
 
diff --git a/gpfsl-examples/graph/ghost.v b/gpfsl-examples/graph/ghost.v
index 5b72b185dd984c4e263f5ef43d2ba0307e77af0a..1549da26a22cfc5b6b693b663b5ef00ffa2e393f 100644
--- a/gpfsl-examples/graph/ghost.v
+++ b/gpfsl-examples/graph/ghost.v
@@ -109,7 +109,7 @@ Lemma ghost_graph_master_agree γ q1 G1 q2 G2  :
   graph_gmaster γ q1 G1 -∗ graph_gmaster γ q2 G2 -∗ ⌜G1 = G2⌝.
 Proof.
   iIntros "o1 o2".
-  iDestruct (own_valid_2 with "o1 o2") as
+  iCombine "o1 o2" gives
     %[[? ?]%mono_list_auth_dfrac_op_valid_L
       [? EqCo%leibniz_equiv_iff]%lat_auth_auth_valid].
   iPureIntro. simplify_eq.
@@ -120,7 +120,7 @@ Lemma ghost_graph_master_snap_included γg q G G' :
   graph_gmaster γg q G -∗ graph_gsnap γg G' -∗ ⌜ G' ⊑ G ⌝.
 Proof.
   iIntros "oM oS".
-  iDestruct (own_valid_2 with "oM oS") as
+  iCombine "oM oS" gives
     %[[? ?]%mono_list_both_dfrac_valid_L [? [??]]%lat_auth_both_valid].
   iPureIntro. by constructor.
 Qed.
diff --git a/gpfsl-examples/gset_disj.v b/gpfsl-examples/gset_disj.v
index 70d9b61da1f7d36da75a936e909b409b00ab7cfb..84e59991bc6b0868dc1d1ccb82ed26834917176e 100644
--- a/gpfsl-examples/gset_disj.v
+++ b/gpfsl-examples/gset_disj.v
@@ -56,7 +56,7 @@ Lemma GsetDisjAuth_frag_include γ q X a :
   GsetDisjAuth γ q X -∗ GsetDisjFrag γ a -∗ ⌜ a ∈ X ⌝.
 Proof.
   iIntros "o1 o2".
-  iDestruct (own_valid_2 with "o1 o2") as
+  iCombine "o1 o2" gives
     %[? [INCL%gset_disj_included%elem_of_subseteq_singleton ?]]%auth_both_dfrac_valid_discrete.
   done.
 Qed.
@@ -86,7 +86,7 @@ Lemma GsetDisjFrag_disj γ a b :
   GsetDisjFrag γ a -∗ GsetDisjFrag γ b -∗ ⌜ a ≠ b ⌝.
 Proof.
   iIntros "o1 o2".
-  iDestruct (own_valid_2 with "o1 o2") as %VALID%auth_frag_valid_1%gset_disj_valid_op.
+  iCombine "o1 o2" gives %VALID%auth_frag_valid_1%gset_disj_valid_op.
   iPureIntro. set_solver.
 Qed.
 End gset_disj.
diff --git a/gpfsl-examples/history/ghost.v b/gpfsl-examples/history/ghost.v
index 9314fe5a3338dba338e2a60576886266c896acfe..a22d686627f70133968b13aac35ab5282a8eb13f 100644
--- a/gpfsl-examples/history/ghost.v
+++ b/gpfsl-examples/history/ghost.v
@@ -81,16 +81,14 @@ Lemma ghost_history_master_agree γ f1 E1 f2 E2  :
   history_gmaster γ f1 E1 -∗ history_gmaster γ f2 E2 -∗ ⌜E1 = E2⌝.
 Proof.
   iIntros "o1 o2".
-  by iDestruct (own_valid_2 with "o1 o2")
-    as %[_ ?%leibniz_equiv]%mono_list_auth_dfrac_op_valid.
+  by iCombine "o1 o2" gives %[_ ?%leibniz_equiv]%mono_list_auth_dfrac_op_valid.
 Qed.
 
 Lemma ghost_history_master_snap_included γg f E E' :
   history_gmaster γg f E -∗ history_gsnap γg E' -∗ ⌜E' ⊑ E⌝.
 Proof.
   iIntros "oM oS".
-  by iDestruct (own_valid_2 with "oM oS")
-      as %[_ ?]%mono_list_both_dfrac_valid_L.
+  by iCombine "oM oS" gives %[_ ?]%mono_list_both_dfrac_valid_L.
 Qed.
 
 (** Graph's Master-Snapshot properties *)
diff --git a/gpfsl-examples/queue/proof_mp2_graph.v b/gpfsl-examples/queue/proof_mp2_graph.v
index 266a234aa2aea7f18f9e2465347f82e3c1af47df..5855d4de8f8344e8bd4b01a724cb907e07a2870b 100644
--- a/gpfsl-examples/queue/proof_mp2_graph.v
+++ b/gpfsl-examples/queue/proof_mp2_graph.v
@@ -284,7 +284,7 @@ Proof using All.
   apply (prefix_lookup _ G.(Es)) in HeV2; [|by destruct SubG0G].
 
   iCombine "◯m ◯m2" as "◯m".
-  iDestruct (own_valid_2 with "●m ◯m") as %[LT%nat_included _]%auth_both_valid_discrete.
+  iCombine "●m ◯m" gives %[LT%nat_included _]%auth_both_valid_discrete.
   have {}LT : (size (com G) ≤ 1)%nat by lia.
 
   iAaccIntro with "QI".
diff --git a/gpfsl-examples/queue/proof_mp_graph.v b/gpfsl-examples/queue/proof_mp_graph.v
index 0f717502259166fcb361552d60304cdb01b234d7..977f32c22a96108c399baacbd169216047bf33e4 100644
--- a/gpfsl-examples/queue/proof_mp_graph.v
+++ b/gpfsl-examples/queue/proof_mp_graph.v
@@ -108,7 +108,7 @@ Proof using All.
     iDestruct "F" as %(SubG' & SubM' & Sub' & Sub'' & IQ & MAX' &
                         EsG' & SoG' & ComG' & EqM' & _).
     rewrite /is_enqueue in IQ. subst enq.
-    iDestruct (own_valid_2 with "nodesA nodes") as %EqL%excl_auth_agree_L.
+    iCombine "nodesA nodes" gives %EqL%excl_auth_agree_L.
     inversion EqL as [EQL].
 
     iMod (own_update_2 with "nodesA nodes") as "[nodesA nodes]".
@@ -155,7 +155,7 @@ Proof using All.
 
     iIntros (v V' G' enqId deqId enq1 deq Venq M') "(QI' & sV' & Local & F)".
     iDestruct "F" as %(SubG' & SubM' & Sub' & Sub'' & CASE).
-    iDestruct (own_valid_2 with "nodes nodes1") as %EqL%excl_auth_agree_L.
+    iCombine "nodes nodes1" gives %EqL%excl_auth_agree_L.
     inversion EqL as [He].
     have He' := He. apply to_set_singleton in He' as [EqeO EQL]. clear EqL.
 
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index a0ad417682f57dbd122a5ee47a4be5fa3029b1cd..288541458ada2c1e74b9ebf052eeacab56d86367 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -1175,7 +1175,7 @@ Lemma LTM_master_snap_included γ T T' :
   LTM_master γ T -∗ LTM_snap γ T' -∗ ⌜T' ⊆ T⌝.
 Proof.
   iIntros "[o1 ?] o2".
-  iDestruct (own_valid_2 with "o1 o2") as %[_ [INCL _]%auth_both_valid_discrete].
+  iCombine "o1 o2" gives %[_ [INCL _]%auth_both_valid_discrete].
   iPureIntro. by move : INCL => /to_agreeM_included.
 Qed.
 Lemma LTM_master_ssnap_lookup γ T η eid :
@@ -1416,7 +1416,7 @@ Proof.
   iIntros "(_ & GM & %γa & MS & QA) (_ & GM' & %γa' & MS' & QA')".
   iDestruct (meta_agree with "MS MS'") as %<-.
   iDestruct (graph_master_agree with "GM GM'") as %<-.
-  iDestruct (own_valid_2 with "QA QA'") as %[_ <-]%frac_agree_op_valid_L. done.
+  iCombine "QA QA'" gives %[_ <-]%frac_agree_op_valid_L. done.
 Qed.
 
 Lemma QueueInv_consistent γg q Q G :
diff --git a/gpfsl-examples/queue/proof_spsc_graph.v b/gpfsl-examples/queue/proof_spsc_graph.v
index 0e953ad581bd636ff9821f45f8a3f58c6effae1a..456e77f0da6ab0c07f3a79bbbebcad55c2553bcd 100644
--- a/gpfsl-examples/queue/proof_spsc_graph.v
+++ b/gpfsl-examples/queue/proof_spsc_graph.v
@@ -113,7 +113,7 @@ Lemma Producer_exclusive N γg γed q G1 G2 M1 M2 es1 es2 :
   Producer N γg γed q G1 M1 es1 -∗ Producer N γg γed q G2 M2 es2 -∗ False.
 Proof.
   iDestruct 1 as "(_ & ◯e1 & _)". iDestruct 1 as "(_ & ◯e2 & _)".
-  by iDestruct (own_valid_2 with "◯e1 ◯e2") as %[?%excl_auth_frag_op_valid ?].
+  by iCombine "◯e1 ◯e2" gives %[?%excl_auth_frag_op_valid ?].
 Qed.
 Lemma Producer_QueueLocal N γg γed q G M es :
   Producer N γg γed q G M es ⊢ wq.(QueueLocal) N γg q G M.
@@ -126,14 +126,14 @@ Lemma Producer_agree N γg γed q G G' M es es' ds :
 Proof.
   iDestruct 1 as "[%xs [QI (●ed & %PERM & %PROD & %CONS & %MATCH & %EMP)]]".
   iDestruct 1 as "(_ & ◯e & _ & _)".
-  by iDestruct (own_valid_2 with "●ed ◯e") as %[<-%excl_auth_agree_L ?].
+  by iCombine "●ed ◯e" gives %[<-%excl_auth_agree_L ?].
 Qed.
 
 Lemma Consumer_exclusive N γg γed q G1 G2 M1 M2 ds1 ds2 :
   Consumer N γg γed q G1 M1 ds1 -∗ Consumer N γg γed q G2 M2 ds2 -∗ False.
 Proof.
   iDestruct 1 as "(_ & ◯d1 & _)". iDestruct 1 as "(_ & ◯d2 & _)".
-  by iDestruct (own_valid_2 with "◯d1 ◯d2") as %[? ?%excl_auth_frag_op_valid].
+  by iCombine "◯d1 ◯d2" gives %[? ?%excl_auth_frag_op_valid].
 Qed.
 Lemma Consumer_QueueLocal N γg γed q G M ds :
   Consumer N γg γed q G M ds ⊢ wq.(QueueLocal) N γg q G M.
@@ -146,7 +146,7 @@ Lemma Consumer_agree N γg γed q G G' M es ds ds' :
 Proof.
   iDestruct 1 as "[%xs [QI (●ed & %PERM & %PROD & %CONS & %MATCH & %EMP)]]".
   iDestruct 1 as "(_ & ◯d & _ & _)".
-  by iDestruct (own_valid_2 with "●ed ◯d") as %[? <-%excl_auth_agree_L].
+  by iCombine "●ed ◯d" gives %[? <-%excl_auth_agree_L].
 Qed.
 
 
@@ -173,7 +173,7 @@ Proof.
   awp_apply (wq.(enqueue_spec) with "⊒V QL"); [done..|].
   iApply (aacc_aupd_commit with "AU"); [done|].
   iIntros (G es ds) "[%xs [QI >(●ed & %PERM & %PROD & %CONS & %MATCH & %EMP)]]".
-  iDestruct (own_valid_2 with "●ed ◯e") as %[<-%excl_auth_agree_L _].
+  iCombine "●ed ◯e" gives %[<-%excl_auth_agree_L _].
   iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC".
   rewrite QueueInv_graph_master_acc. iDestruct "QI" as "[>Gm QI]".
   iDestruct (graph_master_consistent with "Gm") as %EGC.
@@ -248,7 +248,7 @@ Proof.
   awp_apply (wq.(dequeue_spec) with "⊒V QL"); [done..|].
   iApply (aacc_aupd_commit with "AU"); [done|].
   iIntros (G es ds) "[%xs [QI >(●ed & %PERM & %PROD & %CONS & %MATCH & %EMP)]]".
-  iDestruct (own_valid_2 with "●ed ◯d") as %[_ <-%excl_auth_agree_L].
+  iCombine "●ed ◯d" gives %[_ <-%excl_auth_agree_L].
   iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC".
   have [NODUPes [NODUPds NODUPxs]] : NoDup es ∧ NoDup ds ∧ NoDup xs.
   { symmetry in PERM. move: PERM => /ord_nodup.
diff --git a/gpfsl-examples/stack/proof_elim_graph.v b/gpfsl-examples/stack/proof_elim_graph.v
index 8ac136d857583f263dd818a19cc639a01b78b8b3..3b509384464936fb5d8ba165ec1f1fea8f72138c 100644
--- a/gpfsl-examples/stack/proof_elim_graph.v
+++ b/gpfsl-examples/stack/proof_elim_graph.v
@@ -627,14 +627,14 @@ Lemma ge_list_auth_lb_valid γ q T T' :
   ge_list_auth γ q T -∗ ge_list_lb γ T' -∗ ⌜ T' ⊑ T ⌝.
 Proof.
   iIntros "o1 o2".
-  by iDestruct (own_valid_2 with "o1 o2") as %[_ ?]%mono_list_both_dfrac_valid_L.
+  by iCombine "o1 o2" gives %[_ ?]%mono_list_both_dfrac_valid_L.
 Qed.
 
 Lemma ge_list_auth_agree γ q T q' T' :
   ge_list_auth γ q T -∗ ge_list_auth γ q' T' -∗ ⌜ T = T' ⌝.
 Proof.
   iIntros "o1 o2".
-  by iDestruct (own_valid_2 with "o1 o2") as %[_ ?]%mono_list_auth_dfrac_op_valid_L.
+  by iCombine "o1 o2" gives %[_ ?]%mono_list_auth_dfrac_op_valid_L.
 Qed.
 
 Lemma ge_list_alloc T :
diff --git a/gpfsl-examples/stack/proof_mp_client_graph.v b/gpfsl-examples/stack/proof_mp_client_graph.v
index c2eeefc23a5be50dfcf7c1ebe7e99127433ab8a8..0d71bf0983c7c0bb98a4b6fb0e0b8e4cd36aa48e 100644
--- a/gpfsl-examples/stack/proof_mp_client_graph.v
+++ b/gpfsl-examples/stack/proof_mp_client_graph.v
@@ -99,7 +99,7 @@ Section Stack.
       iDestruct "F" as %(SubG' & SubM' & Sub' & Sub'' & IQ & MAX' &
                         EsG' & SoG' & ComG' & EqM' & _).
       rewrite / is_push in IQ. subst push.
-      iDestruct (own_valid_2 with "nodesA nodes") as %[= EQL]%excl_auth_agree_L.
+      iCombine "nodesA nodes" gives %[= EQL]%excl_auth_agree_L.
 
       iMod (own_update_2 with "nodesA nodes") as "[nodesA nodes]".
       { apply (excl_auth_update _ _ (GSet {[pushId]})). }
@@ -143,7 +143,7 @@ Section Stack.
 
       iIntros (v V' G' pushId popId push1 pop Vpush M') "(SI' & sV' & Local & F)".
       iDestruct "F" as %((SubG' & SubM' & Sub' & Sub'') & CASE).
-      iDestruct (own_valid_2 with "nodes nodes1") as %[= He]%excl_auth_agree_L.
+      iCombine "nodes nodes1" gives %[= He]%excl_auth_agree_L.
       have He' := He. apply to_set_singleton in He' as [EqeO EQL].
 
       iMod (own_update_2 with "nodes nodes1") as "[nodes nodes1]".
diff --git a/gpfsl-examples/stack/proof_mp_client_history.v b/gpfsl-examples/stack/proof_mp_client_history.v
index 1d52632aa82f3a6c1ee62f631cebb240fe5b86e1..8e42eac2923858a378170fb4da203b5f94c95900 100644
--- a/gpfsl-examples/stack/proof_mp_client_history.v
+++ b/gpfsl-examples/stack/proof_mp_client_history.v
@@ -98,7 +98,7 @@ Section Stack.
       iIntros (V' E' pushId push Vpush M') "(SI' & sV' & Local & F)".
       iDestruct "F" as %(? & ? & IP & HpushId & HE' & HM').
       rewrite /is_push in IP. subst push.
-      iDestruct (own_valid_2 with "nodesA nodes") as %[= EQL]%excl_auth_agree_L.
+      iCombine "nodesA nodes" gives %[= EQL]%excl_auth_agree_L.
       iMod (own_update_2 with "nodesA nodes") as "[nodesA nodes]".
       { apply (excl_auth_update _ _ (GSet {[pushId]})). }
       iIntros "!>".
@@ -141,7 +141,7 @@ Section Stack.
 
       iIntros (v V' E' pushId popId push1 pop Vpush M') "(SI' & sV' & Local & F)".
       iDestruct "F" as %((? & ?) & CASE).
-      iDestruct (own_valid_2 with "nodes nodes1") as %[= He]%excl_auth_agree_L.
+      iCombine "nodes nodes1" gives %[= He]%excl_auth_agree_L.
       apply to_set_singleton in He as [-> EQL].
       assert (E = [eV]) as ->; last clear EQL.
       { eapply prefix_lookup in Eqe; [|done]. destruct E; [done|].
diff --git a/gpfsl-examples/stack/proof_treiber_graph.v b/gpfsl-examples/stack/proof_treiber_graph.v
index 93df076d7adbdb7ed90bfc50adca3554d4bb5758..4e30ebd839b75883aaf4b3134a5995e62ddf3741 100644
--- a/gpfsl-examples/stack/proof_treiber_graph.v
+++ b/gpfsl-examples/stack/proof_treiber_graph.v
@@ -397,8 +397,7 @@ Lemma LTM_master_snap_included γ q T T' :
 Proof.
   rewrite /LTM_master /LTM_auth.
   iIntros "[o1 ?] o2".
-  iDestruct (own_valid_2 with "o1 o2")
-    as %(_ & INCL & _)%auth_both_dfrac_valid_discrete.
+  iCombine "o1 o2" gives %(_ & INCL & _)%auth_both_dfrac_valid_discrete.
   iPureIntro. by move : INCL => /to_agreeM_included.
 Qed.
 Lemma LTM_master_ssnap_lookup γ q T n eid :
@@ -446,7 +445,7 @@ Lemma LTM_master_agree γ q1 q2 T1 T2 :
   LTM_master γ q1 T1 -∗ LTM_master γ q2 T2 -∗ ⌜ T1 = T2 ⌝.
 Proof.
   iIntros "T1 T2". rewrite /LTM_master /LTM_auth.
-  iDestruct (own_valid_2 with "T1 T2") as %VAL. iPureIntro.
+  iCombine "T1 T2" gives %VAL. iPureIntro.
   move : VAL.
   rewrite (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
   rewrite -auth_frag_op (comm _ (◯ _)) assoc.
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index 3c0446df3cb8f1ba89a5e015bbf0b62bdf6f7c32..9a457b213d53662ecebce27298265df87db9cac2 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -967,8 +967,8 @@ Lemma emo_auth_lb_valid γ esi1 esi2 emo1 emo2 :
     emo2.*1.*2 `prefixes_of` emo1.*1.*2 ⌝.
 Proof.
   iIntros "Hauth Hlb".
-  by iDestruct (own_valid_2 with "Hauth Hlb")
-    as %[[?%mono_list_both_valid_L ?%mono_list_both_valid_L] ?%mono_list_list_both_valid_L].
+  by iCombine "Hauth Hlb"
+    gives %[[?%mono_list_both_valid_L ?%mono_list_both_valid_L] ?%mono_list_list_both_valid_L].
 Qed.
 
 Lemma emo_lb_own_get γ esi emo :
diff --git a/gpfsl-examples/uniq_token.v b/gpfsl-examples/uniq_token.v
index 4adcf5f657ce53b9a44c724f5f86505398f70f3d..471c806d0b27c46b68d1502bcff3a6c336f0aac5 100644
--- a/gpfsl-examples/uniq_token.v
+++ b/gpfsl-examples/uniq_token.v
@@ -52,6 +52,6 @@ Qed.
 Lemma UTok_unique γ : UTok γ -∗ UTok γ -∗ False.
 Proof.
   rewrite UTok_eq. iIntros "U1 U2".
-  by iDestruct (own_valid_2 with "U1 U2") as %?.
+  by iCombine "U1 U2" gives %?.
 Qed.
 End Tok.
diff --git a/gpfsl/algebra/lat_auth.v b/gpfsl/algebra/lat_auth.v
index be22c3b47368b1a3d53fd327ab57a1c76757178b..a8ff17848f3eddb71d2edcc07d97c125fa7aa268 100644
--- a/gpfsl/algebra/lat_auth.v
+++ b/gpfsl/algebra/lat_auth.v
@@ -115,13 +115,13 @@ Context {LAT : latticeT} `{!@LatBottom LAT bot} `{!inG Σ (lat_authR LAT)}.
 Lemma own_master_max γ q a b :
   own γ (●L{q} a) -∗ own γ (◯L b) -∗ ⌜b ⊑ a⌝.
 Proof.
-  iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %[]%lat_auth_both_valid.
+  iIntros "H1 H2". by iCombine "H1 H2" gives %[]%lat_auth_both_valid.
 Qed.
 
 Lemma own_master_eq γ p q a b :
   own γ (●L{p} a) -∗ own γ (●L{q} b) -∗ ⌜a ≡ b⌝.
 Proof.
-  iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %[]%lat_auth_auth_valid.
+  iIntros "H1 H2". by iCombine "H1 H2" gives %[]%lat_auth_auth_valid.
 Qed.
 
 Lemma own_master_update γ a b (Ext : a ⊑ b) :
diff --git a/gpfsl/base_logic/history.v b/gpfsl/base_logic/history.v
index 03e79f0cafe710d67fbbe2f5bc9971130e21613a..0a05f23372658ed6ecb7c6e11d695318106fdeb3 100644
--- a/gpfsl/base_logic/history.v
+++ b/gpfsl/base_logic/history.v
@@ -588,8 +588,8 @@ Section hist.
     iDestruct 1 as (hF V Vc) "(_ & _ & _ & _ & _ & _ & oA & wf)".
     iDestruct "wf" as %(_ & ? & ? & ?).
     rewrite seen_eq. iIntros "oV".
-    iDestruct (own_valid_2 with "oA oV")
-      as %[Le%latT_included _]%auth_both_valid_discrete. simpl in Le.
+    iCombine "oA oV"
+      gives %[Le%latT_included _]%auth_both_valid_discrete. simpl in Le.
     iPureIntro. apply closed_tview_acq_inv. by rewrite Le.
   Qed.
 
diff --git a/gpfsl/base_logic/vprop.v b/gpfsl/base_logic/vprop.v
index 53bac57ae130813997bab4d57885ba8a88f6dfbf..a01b4052182dce4b92b44f526938be792e8ea994 100644
--- a/gpfsl/base_logic/vprop.v
+++ b/gpfsl/base_logic/vprop.v
@@ -541,6 +541,10 @@ Proof. rewrite /IntoSep -view_join_sep=> -> //. Qed.
 #[global] Instance from_sep_view_join P Q1 Q2 V :
   FromSep P Q1 Q2 → FromSep (⊔{V} P) (⊔{V} Q1) (⊔{V} Q2).
 Proof. by rewrite /FromSep -view_join_sep => <-. Qed.
+#[global] Instance maybe_combine_sep_as_view_join P Q1 Q2 V progress :
+  MaybeCombineSepAs P Q1 Q2 progress →
+  MaybeCombineSepAs (⊔{V} P) (⊔{V} Q1) (⊔{V} Q2) progress.
+Proof. by rewrite /MaybeCombineSepAs -view_join_sep => <-. Qed.
 
 #[global] Instance into_or_view_join P Q1 Q2 V :
   IntoOr P Q1 Q2 → IntoOr (⊔{V} P) (⊔{V} Q1) (⊔{V} Q2).
@@ -667,6 +671,10 @@ Proof. rewrite /IntoSep -view_at_sep=> -> //. Qed.
 #[global] Instance from_sep_view_at P Q1 Q2 V :
   FromSep P Q1 Q2 → FromSep (@{V} P) (@{V} Q1) (@{V} Q2).
 Proof. by rewrite /FromSep -view_at_sep => <-. Qed.
+#[global] Instance maybe_combine_sep_as_view_at P Q1 Q2 V progress :
+  MaybeCombineSepAs P Q1 Q2 progress →
+  MaybeCombineSepAs (@{V} P) (@{V} Q1) (@{V} Q2) progress.
+Proof. by rewrite /MaybeCombineSepAs -view_at_sep => <-. Qed.
 
 #[global] Instance into_or_view_at P Q1 Q2 V :
   IntoOr P Q1 Q2 → IntoOr (@{V} P) (@{V} Q1) (@{V} Q2).
diff --git a/gpfsl/gps/model_defs.v b/gpfsl/gps/model_defs.v
index 1d7a6af94ae1b67867b5d315b51678b077286e74..d95c43668fdfcf5c9c7aaa36fce69aa7bb7ef43d 100644
--- a/gpfsl/gps/model_defs.v
+++ b/gpfsl/gps/model_defs.v
@@ -287,7 +287,7 @@ Section Properties.
     gps_own γ χ' -∗ gps_snap γ χ -∗ ⌜ χ ⊆ χ' ⌝.
   Proof.
     iIntros "oA R".
-    iDestruct (own_valid_2 with "oA R") as %VAL.
+    iCombine "oA R" gives %VAL.
     iPureIntro. move : VAL.
     rewrite /stateMap_auth /stateMap_frag -assoc auth_both_valid_discrete /=.
     intros [? _]. apply stateMap_included. etrans; [apply cmra_included_r|done].
diff --git a/gpfsl/logic/na_invariants.v b/gpfsl/logic/na_invariants.v
index 4b9eebe355004ce934a16f4845aba0d0fadeaf73..090ebb98688fb5ac3a3d7864314611d4ae72cf5e 100644
--- a/gpfsl/logic/na_invariants.v
+++ b/gpfsl/logic/na_invariants.v
@@ -72,7 +72,7 @@ Section proofs.
   Proof.
     rewrite /na_own. iIntros "H1 H2".
     iDestruct "H1" as (Vs1) "[H1 _]". iDestruct "H2" as (Vs2) "[H2 _]".
-    iDestruct (own_valid_2 with "H1 H2") as %Hv. iIntros "!%" (i Hi1 Hi2).
+    iCombine "H1 H2" gives %Hv. iIntros "!%" (i Hi1 Hi2).
     specialize (Hv i).
     rewrite /to_ofe_funR /= discrete_fun_lookup_op !decide_True in Hv; auto.
     by destruct Hv.
@@ -130,11 +130,11 @@ Section proofs.
     iDestruct "Htoki" as (Vs) "[Hown #HinVs]".
     iInv N as "[HP|>Htoki]" "Hclose"; last first.
     { iDestruct "Htoki" as (V') "[Hown' _]".
-      iDestruct (own_valid_2 with "Hown Hown'") as %Hv. specialize (Hv i).
+      iCombine "Hown Hown'" gives %Hv. specialize (Hv i).
       rewrite /= discrete_fun_lookup_op discrete_fun_lookup_singleton /to_ofe_funR
         decide_True // in Hv; [by destruct Hv|set_solver-]. }
     iDestruct "HP" as (V') "(HP & >#HV' & >Hdis)".
-    iDestruct (own_valid_2 with "Hown HV'") as %Hv. specialize (Hv i).
+    iCombine "Hown HV'" gives %Hv. specialize (Hv i).
     rewrite /= discrete_fun_lookup_op discrete_fun_lookup_singleton /to_ofe_funR
       decide_True in Hv; [|set_solver].
     apply auth_both_valid_discrete, proj1, latT_included in Hv. simpl in Hv. rewrite [in P _]Hv.
@@ -151,10 +151,10 @@ Section proofs.
     iIntros "!> [HP $]".
     iInv N as "[HP'|>Htoki]" "Hclose".
     { iDestruct "HP'" as (?) "(_ & _ & >Hdis1)".
-      iDestruct (own_valid_2 with "Hdis1 Hdis2")
-        as %[Hv'%option_included _]%auth_both_valid_discrete. exfalso. naive_solver. }
+      iCombine "Hdis1 Hdis2"
+        gives %[Hv'%option_included _]%auth_both_valid_discrete. exfalso. naive_solver. }
     iDestruct "Htoki" as (Vi) "[Hown Hdis1]".
-    iDestruct (own_valid_2 with "Hdis1 Hdis2") as %EQVi%excl_auth_agree%(inj to_latT).
+    iCombine "Hdis1 Hdis2" gives %EQVi%excl_auth_agree%(inj to_latT).
     (* FIXME : rewrite EQVi should work. *)
     assert (@discrete_fun_singleton _ _ (λ _, _) i (● to_latT Vi) ≡
             discrete_fun_singleton i (● to_latT (Vs i))) as -> by by f_equiv; rewrite EQVi.
diff --git a/gpfsl/logic/readonly_ptsto.v b/gpfsl/logic/readonly_ptsto.v
index e30b3ad89b1fe40b80bcec199aee938c4f8a8900..af767f91396ceb5a7c16dec7c29f8cfba306aea7 100644
--- a/gpfsl/logic/readonly_ptsto.v
+++ b/gpfsl/logic/readonly_ptsto.v
@@ -73,7 +73,7 @@ Proof.
   rewrite ROSeen_eq.
   iDestruct 1 as (??) "[_ O1]". iDestruct 1 as (??) "[_ O2]".
   rewrite !view_at_objective_iff.
-  iDestruct (own_valid_2 with "O1 O2") as %?%to_agree_op_valid_L.
+  iCombine "O1 O2" gives %?%to_agree_op_valid_L.
   iPureIntro. by simplify_eq.
 Qed.
 Lemma ROSeen_agree_l l γ v v' V :
@@ -102,7 +102,7 @@ Proof.
   rewrite ROPtsTo_eq ROSeen_eq.
   iDestruct 1 as (???????) "(_&_&_&O1)". iDestruct 1 as (??) "[_ O2]".
   rewrite !view_at_objective_iff.
-  iDestruct (own_valid_2 with "O1 O2") as %?%to_agree_op_valid_L.
+  iCombine "O1 O2" gives %?%to_agree_op_valid_L.
   iPureIntro. by simplify_eq.
 Qed.
 Lemma ROPtsTo_ROSeen_agree_l l γ v v' V :
@@ -167,7 +167,7 @@ Proof.
   iDestruct "Pts" as (t m rsa rns ws Va (GH & Eqv' & LeVa))
             "((SLV & ARL & AWL & NAL) & HC & (AR & AW & NA) & AR1)".
   iDestruct "SR" as (t' V') "[SLV' AR2]".
-  iDestruct (own_valid_2 with "AR1 AR2") as %Eq'%to_agree_op_valid_L.
+  iCombine "AR1 AR2" gives %Eq'%to_agree_op_valid_L.
   inversion Eq'; clear Eq'; subst t' v' V'.
 
   iDestruct (seen_time_AllocLocal_singleton l t m with "[SLV']") as %AL.
@@ -215,7 +215,7 @@ Proof.
   iDestruct "Pts" as (t m rsa rns ws Va (GH & Eqv' & LeVa))
             "((SLV & ARL & #AWL & NAL) & HC & (AR & AW & NA) & AR1)".
   iDestruct "SR" as (t' V') "[SLV' AR2]".
-  iDestruct (own_valid_2 with "AR1 AR2") as %Eq'%to_agree_op_valid_L.
+  iCombine "AR1 AR2" gives %Eq'%to_agree_op_valid_L.
   inversion Eq'; clear Eq'; subst t' v' V'.
   iDestruct (seen_time_AllocLocal_singleton l t m with "[SLV']") as %AL.
   { by inversion Eqv'. } { iDestruct (seen_view_seen_time with "SLV'") as "[$ ?]". }
diff --git a/gpfsl/logic/relacq.v b/gpfsl/logic/relacq.v
index 2e3183238a144a80abb8a9b6e471e192298571c0..d7dc2427eeb4e400a007d06fe8ede7b5108bb8af 100644
--- a/gpfsl/logic/relacq.v
+++ b/gpfsl/logic/relacq.v
@@ -507,6 +507,10 @@ Section proofmode.
   Global Instance from_sep_rel_mod P Q1 Q2 tid :
     FromSep P Q1 Q2 → FromSep (△{tid} P) (△{tid} Q1) (△{tid} Q2).
   Proof. by rewrite /FromSep rel_sep => ->. Qed.
+  Global Instance maybe_combine_sep_as_rel_mod P Q1 Q2 tid progress :
+    MaybeCombineSepAs P Q1 Q2 progress →
+    MaybeCombineSepAs (△{tid} P) (△{tid} Q1) (△{tid} Q2) progress.
+  Proof. by rewrite /MaybeCombineSepAs rel_sep => ->. Qed.
 
   Global Instance into_or_rel_mod P Q1 Q2 tid :
     IntoOr P Q1 Q2 → IntoOr (△{tid} P) (△{tid} Q1) (△{tid} Q2).
@@ -574,6 +578,10 @@ Section proofmode.
   Global Instance from_sep_acq_mod P Q1 Q2 tid :
     FromSep P Q1 Q2 → FromSep (▽{tid} P) (▽{tid} Q1) (▽{tid} Q2).
   Proof. by rewrite /FromSep acq_sep => ->. Qed.
+  Global Instance maybe_combine_sep_as_acq_mod P Q1 Q2 tid progress :
+    MaybeCombineSepAs P Q1 Q2 progress →
+    MaybeCombineSepAs (▽{tid} P) (▽{tid} Q1) (▽{tid} Q2) progress.
+  Proof. by rewrite /MaybeCombineSepAs acq_sep => ->. Qed.
 
   Global Instance into_or_acq_mod P Q1 Q2 tid :
     IntoOr P Q1 Q2 → IntoOr (▽{tid} P) (▽{tid} Q1) (▽{tid} Q2).
diff --git a/gpfsl/logic/view_invariants.v b/gpfsl/logic/view_invariants.v
index 231b7d8414fd321e0f4cde76c8c1c48099991772..21b8cbcbe583cdc1e2020ea64b826efe7ba9ba92 100644
--- a/gpfsl/logic/view_invariants.v
+++ b/gpfsl/logic/view_invariants.v
@@ -162,7 +162,8 @@ Proof.
   iMod (inv_acc with "Inv") as "[VI Closed]"; [done|].
   iDestruct "VI" as (V') "[>tok'|[>oA P]]".
   { rewrite view_tok_eq. iDestruct "tok'" as (V2) "[_ tok']".
-    by iDestruct (own_valid_2 with "tok [$tok']") as %[? _]%frac_auth_frag_valid. }
+    rewrite view_at_embed.
+    by iCombine "tok tok'" gives %[? _]%frac_auth_frag_valid. }
   iDestruct (own_valid_2 with "[$oA] tok")
     as %->%frac_auth_agree%to_latT_inj%leibniz_equiv_iff.
   iMod ("Closed" with "[tok]").
@@ -196,8 +197,8 @@ Proof.
   iSplitL "P". { rewrite view_join_later. by iFrame. }
   iFrame "oA". iSplitL "".
   { iIntros "!>". iDestruct 1 as (V3) "[In3 tok]". iIntros "oA".
-    iDestruct (own_valid_2 with "oA tok")
-      as %->%frac_auth_agree%to_latT_inj%leibniz_equiv_iff.
+    iCombine "oA tok"
+      gives %->%frac_auth_agree%to_latT_inj%leibniz_equiv_iff.
     by iFrame. }
   iIntros "oA". iSplit; last iSplit.
   - iDestruct 1 as (V3) "[#In3 tok]". iIntros "P".
@@ -225,8 +226,8 @@ Proof.
     iExists (V' ⊔ V3). iRight. rewrite view_at_view_join.
     iNext. by iFrame.
   - iDestruct 1 as (V3) "[#In3 tok]". iSplit.
-    + iDestruct (own_valid_2 with "oA tok")
-        as %->%frac_auth_agree%to_latT_inj%leibniz_equiv_iff.
+    + iCombine "oA tok"
+        gives %->%frac_auth_agree%to_latT_inj%leibniz_equiv_iff.
       by iFrame.
     + iMod ("Closed" with "[tok]"); [|done].
       iExists V3. iLeft. rewrite view_tok_eq. iExists V3. by iFrame "tok".