diff --git a/CHANGELOG.md b/CHANGELOG.md
index dac4e1a0d516f559def5343f72e41f7e10a83274..efb51c925ff73267f87c2d6d7656f55ab2ba0318 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -44,6 +44,19 @@ Coq 8.13 is no longer supported.
   intuitionistic. This means that tactics such as `iDestruct ... as "->"` will
   not dispose of hypotheses to perform the rewrite.
 * Remove tactic `iSolveTC` in favor of `tc_solve` in std++.
+* The result of `iCombine` is no longer computed with the `FromSep` typeclass,
+  but with a new `CombineSepAs` typeclass. If you provide custom `FromSep`
+  instances and use the `iCombine` tactic, you will need to define additional
+  `CombineSepAs` instances. This is done in preparation for making `iCombine`
+  combine propositions in ways that are not appropriate for how `FromSep` is used.
+  Note that `FromSep` is still used for determining the new goals when applying
+  the `iSplitL` and `iSplitR` tactics.
+* The `iCombine` tactic now accepts an (optional) 'gives' clause, with which one
+  can learn persistent facts from the combination of two hypotheses. One can
+  register such 'gives' clauses by providing instances of the new
+  `CombineSepGives` typeclass. The 'gives' clause is still experimental;
+  in future versions of Iris it will combine `own` connectives based on the
+  validity rules for cameras.
 
 **Changes in `base_logic`:**
 
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index aa3c6441747d4f605e081706129356b9f51d9c65..92b47ddfbf9b3b97cd5cd623c237fa0d14675b8e 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -184,10 +184,17 @@ Separation logic-specific tactics
 - `iFrame select (pat)%I` : cancel the last hypothesis of the intuitionistic
   of spatial context that matches pattern `pat`.
 - `iCombine "H1 H2" as "ipat"` : combine `H1 : P1` and `H2 : P2` into `H: P1 ∗
-  P2` or something simplified but equivalent, then destruct the combined
+  P2` or something simplified but equivalent, then `destruct` the combined
   hypothesis using `ipat`. Some examples of simplifications `iCombine` knows
   about are to combine `own γ x` and `own γ y` into `own γ (x ⋅ y)`, and to
   combine `l ↦{1/2} v` and `l ↦{1/2} v` into `l ↦ v`.
+- `iCombine "H1 H2" gives "ipat"` : from `H1 : P1` and `H2 : P2`, find
+  persistent consequences of `P1 ∗ P2`, then `destruct` this consequence with
+  `ipat`. Some examples of persistent consequences `iCombine` knows about are
+  that `own γ x` and `own γ y` gives `✓ (x ⋅ y)`, and that
+  `l ↦{#q1} v1` and `l ↦{#q2} v2` gives `⌜(q1 + q2 ≤ 1) ∧ v1 = v2⌝`.
+- `iCombine "H1 H2" as "ipat1" gives "ipat2"` combines the two functionalities
+  of `iCombine` described above.
 - `iAccu` : solve a goal that is an evar by instantiating it with all
   hypotheses from the spatial context joined together with a separating
   conjunction (or `emp` in case the spatial context is empty). Not commonly
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 593635cc6e1a0de6b1f4792b5252f2412b84d7ab..8c3860778aa2b20b5288c522126cfc576ee2144d 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -157,10 +157,25 @@ Section gen_heap.
   Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
   Proof. rewrite mapsto_unseal. apply ghost_map_elem_agree. Qed.
 
+  Global Instance mapsto_combine_sep_gives l dq1 dq2 v1 v2 : 
+    CombineSepGives (l ↦{dq1} v1) (l ↦{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝ | 30.
+  Proof.
+    rewrite /CombineSepGives. iIntros "[H1 H2]".
+    iDestruct (mapsto_valid_2 with "H1 H2") as %?. eauto.
+  Qed.
+
   Lemma mapsto_combine l dq1 dq2 v1 v2 :
     l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
   Proof. rewrite mapsto_unseal. apply ghost_map_elem_combine. Qed.
 
+  Global Instance mapsto_combine_as l dq1 dq2 v1 v2 :
+    CombineSepAs (l ↦{dq1} v1) (l ↦{dq2} v2) (l ↦{dq1 ⋅ dq2} v1) | 60. 
+    (* higher cost than the Fractional instance, which kicks in for #qs *)
+  Proof.
+    rewrite /CombineSepAs. iIntros "[H1 H2]".
+    iDestruct (mapsto_combine with "H1 H2") as "[$ _]".
+  Qed.
+
   Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
     ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
   Proof. rewrite mapsto_unseal. apply ghost_map_elem_frac_ne. Qed.
@@ -198,8 +213,8 @@ Section gen_heap.
   Proof.
     rewrite meta_token_unseal /meta_token_def.
     iIntros "(%γm1 & #Hγm1 & Hm1) (%γm2 & #Hγm2 & Hm2)".
-    iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
-    iDestruct (own_valid_2 with "Hm1 Hm2") as %?%reservation_map_token_valid_op.
+    iCombine "Hγm1 Hγm2" gives %[_ ->].
+    iCombine "Hm1 Hm2" gives %?%reservation_map_token_valid_op.
     iExists γm2. iFrame "Hγm2". rewrite reservation_map_token_union //. by iSplitL "Hm1".
   Qed.
   Lemma meta_token_union l E1 E2 :
@@ -221,8 +236,8 @@ Section gen_heap.
   Proof.
     rewrite meta_unseal /meta_def.
     iIntros "(%γm1 & Hγm1 & Hm1) (%γm2 & Hγm2 & Hm2)".
-    iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
-    iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
+    iCombine "Hγm1 Hγm2" gives %[_ ->].
+    iCombine "Hm1 Hm2" gives %Hγ; iPureIntro.
     move: Hγ. rewrite -reservation_map_data_op reservation_map_data_valid.
     move=> /to_agree_op_inv_L. naive_solver.
   Qed.
@@ -274,7 +289,7 @@ Section gen_heap.
   Proof.
     iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
     rewrite /gen_heap_interp mapsto_unseal.
-    by iDestruct (ghost_map_lookup with "Hσ Hl") as %?.
+    by iCombine "Hσ Hl" gives %?.
   Qed.
 
   Lemma gen_heap_update σ l v1 v2 :
@@ -282,7 +297,7 @@ Section gen_heap.
   Proof.
     iDestruct 1 as (m Hσm) "[Hσ Hm]".
     iIntros "Hl". rewrite /gen_heap_interp mapsto_unseal /mapsto_def.
-    iDestruct (ghost_map_lookup with "Hσ Hl") as %Hl.
+    iCombine "Hσ Hl" gives %Hl.
     iMod (ghost_map_update with "Hσ Hl") as "[Hσ Hl]".
     iModIntro. iFrame "Hl". iExists m. iFrame.
     iPureIntro. apply elem_of_dom_2 in Hl.
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index d88c997566f8787fe9764f55d19d68082c947eae..51412d1e28ebe7979768048f996d13235f8c0fea 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -139,7 +139,7 @@ Section inv_heap.
     ⌜∃ v I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
   Proof.
     iIntros "Hl_inv Hâ—¯".
-    iDestruct (own_valid_2 with "Hâ—¯ Hl_inv") as %[Hincl Hvalid]%auth_both_valid_discrete.
+    iCombine "Hâ—¯ Hl_inv" gives %[Hincl Hvalid]%auth_both_valid_discrete.
     iPureIntro.
     move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
     apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & _ & HI & Hh).
@@ -152,7 +152,7 @@ Section inv_heap.
     ⌜ ∃ I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
   Proof.
     iIntros "Hl_inv H●".
-    iDestruct (own_valid_2 with "H● Hl_inv") as %[Hincl Hvalid]%auth_both_valid_discrete.
+    iCombine "H● Hl_inv" gives %[Hincl Hvalid]%auth_both_valid_discrete.
     iPureIntro.
     move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
     apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & -> & HI & Hh).
@@ -203,7 +203,7 @@ Section inv_heap.
     destruct (h !! l) as [v'| ] eqn: Hlookup.
     - (* auth map contains l --> contradiction *)
       iDestruct (big_sepM_lookup with "HsepM") as "[_ Hl']"; first done.
-      by iDestruct (mapsto_valid_2 with "Hl Hl'") as %[??].
+      by iCombine "Hl Hl'" gives %[??].
     - iMod (own_update with "H●") as "[H● H◯]".
       { apply lookup_to_inv_heap_None in Hlookup.
         apply (auth_update_alloc _
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index 2a9aa9744440d756bfdd0065918246a9cfcce194..2ebcbaa930830591abec7aafe45bbeaa34b8eda0 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -87,7 +87,7 @@ Section lemmas.
     k ↪[γ]{dq1} v1 -∗ k ↪[γ]{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %?%gmap_view_frag_op_valid_L.
+    iCombine "H1 H2" gives %?%gmap_view_frag_op_valid_L.
     done.
   Qed.
   Lemma ghost_map_elem_agree k γ dq1 dq2 v1 v2 :
@@ -98,6 +98,14 @@ Section lemmas.
     done.
   Qed.
 
+  Global Instance ghost_map_elem_combine_gives γ k v1 dq1 v2 dq2 : 
+    CombineSepGives (k ↪[γ]{dq1} v1) (k ↪[γ]{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
+  Proof.
+    rewrite /CombineSepGives. iIntros "[H1 H2]".
+    iDestruct (ghost_map_elem_valid_2 with "H1 H2") as %[H1 H2].
+    eauto.
+  Qed.
+
   Lemma ghost_map_elem_combine k γ dq1 dq2 v1 v2 :
     k ↪[γ]{dq1} v1 -∗ k ↪[γ]{dq2} v2 -∗ k ↪[γ]{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
   Proof.
@@ -105,11 +113,20 @@ Section lemmas.
     unseal. iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
   Qed.
 
+  Global Instance ghost_map_elem_combine_as k γ dq1 dq2 v1 v2 :
+    CombineSepAs (k ↪[γ]{dq1} v1) (k ↪[γ]{dq2} v2) (k ↪[γ]{dq1 ⋅ dq2} v1) | 60. 
+    (* higher cost than the Fractional instance [combine_sep_fractional_bwd],
+       which kicks in for #qs *)
+  Proof.
+    rewrite /CombineSepAs. iIntros "[H1 H2]".
+    iDestruct (ghost_map_elem_combine with "H1 H2") as "[$ _]".
+  Qed.
+
   Lemma ghost_map_elem_frac_ne γ k1 k2 dq1 dq2 v1 v2 :
     ¬ ✓ (dq1 ⋅ dq2) → k1 ↪[γ]{dq1} v1 -∗ k2 ↪[γ]{dq2} v2 -∗ ⌜k1 ≠ k2⌝.
   Proof.
     iIntros (?) "H1 H2"; iIntros (->).
-    by iDestruct (ghost_map_elem_valid_2 with "H1 H2") as %[??].
+    by iCombine "H1 H2" gives %[??].
   Qed.
   Lemma ghost_map_elem_ne γ k1 k2 dq2 v1 v2 :
     k1 ↪[γ] v1 -∗ k2 ↪[γ]{dq2} v2 -∗ ⌜k1 ≠ k2⌝.
@@ -173,7 +190,7 @@ Section lemmas.
     ghost_map_auth γ q1 m1 -∗ ghost_map_auth γ q2 m2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ m1 = m2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_auth_dfrac_op_valid_L.
+    iCombine "H1 H2" gives %[??]%gmap_view_auth_dfrac_op_valid_L.
     done.
   Qed.
   Lemma ghost_map_auth_agree γ q1 q2 m1 m2 :
@@ -189,10 +206,23 @@ Section lemmas.
     ghost_map_auth γ q m -∗ k ↪[γ]{dq} v -∗ ⌜m !! k = Some v⌝.
   Proof.
     unseal. iIntros "Hauth Hel".
-    iDestruct (own_valid_2 with "Hauth Hel") as %[?[??]]%gmap_view_both_dfrac_valid_L.
+    iCombine "Hauth Hel" gives %[?[??]]%gmap_view_both_dfrac_valid_L.
     eauto.
   Qed.
 
+  Global Instance ghost_map_lookup_combine_gives_1 {γ q m k dq v} :
+    CombineSepGives (ghost_map_auth γ q m) (k ↪[γ]{dq} v) ⌜m !! k = Some v⌝.
+  Proof.
+    rewrite /CombineSepGives. iIntros "[H1 H2]".
+    iDestruct (ghost_map_lookup with "H1 H2") as %->. eauto.
+  Qed.
+
+  Global Instance ghost_map_lookup_combine_gives_2 {γ q m k dq v} :
+    CombineSepGives (k ↪[γ]{dq} v) (ghost_map_auth γ q m) ⌜m !! k = Some v⌝.
+  Proof.
+    rewrite /CombineSepGives comm. apply ghost_map_lookup_combine_gives_1.
+  Qed.
+
   Lemma ghost_map_insert {γ m} k v :
     m !! k = None →
     ghost_map_auth γ 1 m ==∗ ghost_map_auth γ 1 (<[k := v]> m) ∗ k ↪[γ] v.
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 56e720fd2352b23862c3d074917007f5fb42c20b..6139e4088723542fec3cfc38f1f56ed3dc6425cd 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -1,6 +1,6 @@
 (** A simple "ghost variable" of arbitrary type with fractional ownership.
 Can be mutated when fully owned. *)
-From iris.algebra Require Import dfrac_agree.
+From iris.algebra Require Import dfrac_agree proofmode_classes frac.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export own.
@@ -55,7 +55,7 @@ Section lemmas.
     ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ a1 = a2⌝.
   Proof.
     unseal. iIntros "Hvar1 Hvar2".
-    iDestruct (own_valid_2 with "Hvar1 Hvar2") as %[Hq Ha]%frac_agree_op_valid.
+    iCombine "Hvar1 Hvar2" gives %[Hq Ha]%frac_agree_op_valid.
     done.
   Qed.
   (** Almost all the time, this is all you really need. *)
@@ -66,6 +66,26 @@ Section lemmas.
     iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ?]. done.
   Qed.
 
+  Global Instance ghost_var_combine_gives γ a1 q1 a2 q2 :
+    CombineSepGives (ghost_var γ q1 a1) (ghost_var γ q2 a2)
+      ⌜(q1 + q2 ≤ 1)%Qp ∧ a1 = a2⌝.
+  Proof.
+    rewrite /CombineSepGives. iIntros "[H1 H2]".
+    iDestruct (ghost_var_valid_2 with "H1 H2") as %[H1 H2].
+    eauto.
+  Qed.
+
+  Global Instance ghost_var_combine_as γ a1 q1 a2 q2 q :
+    IsOp q q1 q2 →
+    CombineSepAs (ghost_var γ q1 a1) (ghost_var γ q2 a2)
+      (ghost_var γ q a1) | 60.
+  (* higher cost than the Fractional instance, which is used for a1 = a2 *)
+  Proof.
+    rewrite /CombineSepAs /IsOp => ->. iIntros "[H1 H2]".
+    iCombine "H1 H2" gives %[_ ->].
+    by iCombine "H1 H2" as "H".
+  Qed.
+
   (** This is just an instance of fractionality above, but that can be hard to find. *)
   Lemma ghost_var_split γ a q1 q2 :
     ghost_var γ (q1 + q2) a -∗ ghost_var γ q1 a ∗ ghost_var γ q2 a.
diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index 402144c42b7b012b0eaee2d34521d49ea6dec368..4bc86a85783092dfaa04a61ff628e1f0b7e2a775 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -83,7 +83,7 @@ Section gset_bij.
     ⌜✓ (dq1 ⋅ dq2) ∧ L1 = L2 ∧ gset_bijective L1⌝.
   Proof.
     rewrite gset_bij_own_auth_eq. iIntros "H1 H2".
-    by iDestruct (own_valid_2 with "H1 H2") as %?%gset_bij_auth_dfrac_op_valid.
+    by iCombine "H1 H2" gives %?%gset_bij_auth_dfrac_op_valid.
   Qed.
   Lemma gset_bij_own_auth_exclusive γ L1 L2 :
     gset_bij_own_auth γ (DfracOwn 1) L1 -∗ gset_bij_own_auth γ (DfracOwn 1) L2 -∗ False.
@@ -104,7 +104,7 @@ Section gset_bij.
     ⌜a = a' ↔ b = b'⌝.
   Proof.
     rewrite gset_bij_own_elem_eq. iIntros "Hel1 Hel2".
-    by iDestruct (own_valid_2 with "Hel1 Hel2") as %?%gset_bij_elem_agree.
+    by iCombine "Hel1 Hel2" gives %?%gset_bij_elem_agree.
   Qed.
 
   Lemma gset_bij_own_elem_get {γ q L} a b :
@@ -119,7 +119,7 @@ Section gset_bij.
     gset_bij_own_auth γ q L -∗ gset_bij_own_elem γ a b -∗ ⌜(a, b) ∈ L⌝.
   Proof.
     iIntros "Hauth Helem". rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
-    iPoseProof (own_valid_2 with "Hauth Helem") as "%Ha".
+    iCombine "Hauth Helem" gives "%Ha".
     iPureIntro. revert Ha. rewrite bij_both_dfrac_valid. intros (_ & _ & ?); done.
   Qed.
 
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index c92fdb22240c2d0d563b377227b6c2e32eb588a5..5f27454f6f71b8ed515711dd224d1dd5b98ff9ad 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -69,7 +69,7 @@ Section later_credit_theory.
     rewrite lc_unseal /lc_def.
     rewrite lc_supply_unseal /lc_supply_def.
     iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as "%Hop".
+    iCombine "H1 H2" gives %Hop.
     iPureIntro. eapply auth_both_valid_discrete in Hop as [Hlt _].
     by eapply nat_included.
   Qed.
@@ -117,6 +117,19 @@ Section later_credit_theory.
   Proof.
     by rewrite /FromSep (lc_succ n).
   Qed.
+  (** When combining later credits with [iCombine], the priorities are
+  reversed when compared to [FromSep] and [IntoSep]. This causes
+  [£ n] and [£ 1] to be combined as [£ (S n)], not as [£ (n + 1)]. *)
+  Global Instance combine_sep_lc_add n m :
+    CombineSepAs (£ n) (£ m) (£ (n + m)) | 1.
+  Proof.
+    by rewrite /CombineSepAs lc_split.
+  Qed.
+  Global Instance combine_sep_lc_S_l n :
+    CombineSepAs (£ n) (£ 1) (£ (S n)) | 0.
+  Proof.
+    by rewrite /CombineSepAs comm (lc_succ n).
+  Qed.
 
   Global Instance into_sep_lc_add n m :
     IntoSep (£ (n + m)) (£ n) (£ m) | 0.
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 02df5fafe8b8519e3299fa845e8d80770aba1f13..353b262a76599f5f0bf0f4eca69d459f15bd65b1 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -67,7 +67,7 @@ Section mono_nat.
     ⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_dfrac_op_valid; done.
+    iCombine "H1 H2" gives %?%mono_nat_auth_dfrac_op_valid; done.
   Qed.
   Lemma mono_nat_auth_own_exclusive γ n1 n2 :
     mono_nat_auth_own γ 1 n1 -∗ mono_nat_auth_own γ 1 n2 -∗ False.
@@ -80,7 +80,7 @@ Section mono_nat.
     mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ m -∗ ⌜(q ≤ 1)%Qp ∧ m ≤ n⌝.
   Proof.
     unseal. iIntros "Hauth Hlb".
-    iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mono_nat_both_dfrac_valid.
+    iCombine "Hauth Hlb" gives %Hvalid%mono_nat_both_dfrac_valid.
     auto.
   Qed.
 
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index 627c41865e389c8287a331a8a89b428df0e09792..0c549c2a00d0e7284d763943ce2e1157cb619f06 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -103,7 +103,7 @@ Section proofs.
     - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
       iIntros "!> [HP $]".
       iInv N as "[[_ >Hdis2]|>Hitok]".
-      + iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op].
+      + iCombine "Hdis Hdis2" gives %[_ Hval%gset_disj_valid_op].
         set_solver.
       + iSplitR "Hitok"; last by iFrame. eauto with iFrame.
     - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 9497fb0b3a8066e195e389485ffd46990a7de4fd..71f9f9bcf38d5cfeee92583037bcdd10f2f00e3e 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -372,6 +372,19 @@ Section proofmode_instances.
   Global Instance from_sep_own γ a b1 b2 :
     IsOp a b1 b2 → FromSep (own γ a) (own γ b1) (own γ b2).
   Proof. intros. by rewrite /FromSep -own_op -is_op. Qed.
+  (* TODO: Improve this instance with generic own simplification machinery
+  once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
+  Global Instance combine_sep_as_own γ a b1 b2 :
+    IsOp a b1 b2 → CombineSepAs (own γ b1) (own γ b2) (own γ a).
+  Proof. intros. by rewrite /CombineSepAs -own_op -is_op. Qed.
+  (* TODO: Improve this instance with generic own validity simplification
+  machinery once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
+  Global Instance combine_sep_gives_own γ b1 b2 :
+    CombineSepGives (own γ b1) (own γ b2) (✓ (b1 ⋅ b2)).
+  Proof.
+    intros. rewrite /CombineSepGives -own_op own_valid.
+    by apply: bi.persistently_intro.
+  Qed.
   Global Instance from_and_own_persistent γ a b1 b2 :
     IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
     FromAnd (own γ a) (own γ b1) (own γ b2).
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index 3d3e94de4be5160c686948dacd06ef55d49e18cc..9bb346154e95f5a1efc10b652c777b22e53fa83a 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -122,7 +122,7 @@ Section proph_map.
   Proof.
     iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
     rewrite /proph_map_interp proph_unseal /proph_def.
-    iDestruct (ghost_map_lookup with "H● Hp") as %HR.
+    iCombine "H● Hp" gives %HR.
     assert (vs = v :: proph_list_resolves pvs p) as ->.
     { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
     iMod (ghost_map_update (proph_list_resolves pvs p) with "H● Hp") as "[H● H◯]".
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 23bbf4a068978973ee4aab2a5482c7432b2bdf25..d78afdc79b8c757a3223518868d190857b9a21b6 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -75,13 +75,32 @@ Section saved_anything.
     saved_anything_own γ dq1 x -∗ saved_anything_own γ dq2 y -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ x ≡ y.
   Proof.
     iIntros "Hx Hy". rewrite /saved_anything_own.
-    iDestruct (own_valid_2 with "Hx Hy") as "Hv".
+    iCombine "Hx Hy" gives "Hv".
     rewrite dfrac_agree_validI_2. iDestruct "Hv" as "[$ $]".
   Qed.
   Lemma saved_anything_agree γ dq1 dq2 x y :
     saved_anything_own γ dq1 x -∗ saved_anything_own γ dq2 y -∗ x ≡ y.
   Proof. iIntros "Hx Hy". iPoseProof (saved_anything_valid_2 with "Hx Hy") as "[_ $]". Qed.
 
+  Global Instance saved_anything_combine_gives γ dq1 dq2 x y :
+    CombineSepGives (saved_anything_own γ dq1 x) (saved_anything_own γ dq2 y)
+      (⌜✓ (dq1 ⋅ dq2)⌝ ∗ x ≡ y).
+  Proof.
+    rewrite /CombineSepGives. iIntros "[Hx Hy]".
+    iPoseProof (saved_anything_valid_2 with "Hx Hy") as "[% #$]". eauto.
+  Qed.
+
+  Global Instance saved_anything_combine_as γ dq1 dq2 x y :
+    CombineSepAs (saved_anything_own γ dq1 x) (saved_anything_own γ dq2 y)
+      (saved_anything_own γ (dq1 ⋅ dq2) x).
+  (* higher cost than the Fractional instance, which kicks in for #qs *)
+  Proof.
+    rewrite /CombineSepAs. iIntros "[Hx Hy]".
+    iCombine "Hx Hy" gives "[_ #H]".
+    iRewrite -"H" in "Hy". rewrite /saved_anything_own.
+    iCombine "Hx Hy" as "Hxy". by rewrite -dfrac_agree_op.
+  Qed.
+
   (** Make an element read-only. *)
   Lemma saved_anything_persist γ dq v :
     saved_anything_own γ dq v ==∗ saved_anything_own γ DfracDiscarded v.
@@ -161,12 +180,12 @@ Section saved_prop.
     saved_prop_own γ dq1 P -∗ saved_prop_own γ dq2 Q -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ ▷ (P ≡ Q).
   Proof.
     iIntros "HP HQ".
-    iPoseProof (saved_anything_valid_2 (F := ▶ ∙) with "HP HQ") as "($ & Hag)".
+    iCombine "HP HQ" gives "($ & Hag)".
     by iApply later_equivI.
   Qed.
   Lemma saved_prop_agree γ dq1 dq2 P Q :
     saved_prop_own γ dq1 P -∗ saved_prop_own γ dq2 Q -∗ ▷ (P ≡ Q).
-  Proof. iIntros "HP HQ". iPoseProof (saved_prop_valid_2 with "HP HQ") as "[_ $]". Qed.
+  Proof. iIntros "HP HQ". iCombine "HP" "HQ" gives "[_ $]". Qed.
 
   (** Make an element read-only. *)
   Lemma saved_prop_persist γ dq P :
@@ -239,7 +258,7 @@ Section saved_pred.
     saved_pred_own γ dq1 Φ -∗ saved_pred_own γ dq2 Ψ -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ ▷ (Φ x ≡ Ψ x).
   Proof.
     iIntros "HΦ HΨ".
-    iPoseProof (saved_anything_valid_2 (F := A -d> ▶ ∙) with "HΦ HΨ") as "($ & Hag)".
+    iCombine "HΦ HΨ" gives "($ & Hag)".
     iApply later_equivI. by iApply (discrete_fun_equivI with "Hag").
   Qed.
   Lemma saved_pred_agree γ dq1 dq2 Φ Ψ x :
diff --git a/iris/base_logic/proofmode.v b/iris/base_logic/proofmode.v
index 731ec300570a2219ab3613718d587d0cf606ff5d..019b9f024e78d1347e53e1d66e998f49972532d3 100644
--- a/iris/base_logic/proofmode.v
+++ b/iris/base_logic/proofmode.v
@@ -24,6 +24,20 @@ Section class_instances.
     IsOp a b1 b2 →
     FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
   Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
+  (* TODO: Improve this instance with generic own simplification machinery
+  once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
+  Global Instance combine_sep_as_ownM (a b1 b2 : M) :
+    IsOp a b1 b2 →
+    CombineSepAs (uPred_ownM b1) (uPred_ownM b2) (uPred_ownM a).
+  Proof. intros. by rewrite /CombineSepAs -ownM_op -is_op. Qed.
+  (* TODO: Improve this instance with generic own validity simplification
+  machinery once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
+  Global Instance combine_sep_gives_ownM (b1 b2 : M) :
+    CombineSepGives (uPred_ownM b1) (uPred_ownM b2) (✓ (b1 ⋅ b2)).
+  Proof.
+    intros. rewrite /CombineSepGives -ownM_op ownM_valid.
+    by apply: bi.persistently_intro.
+  Qed.
   Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
     IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
     FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 05917ee57d6eafc63eb15ae736fe84ac37511165..2beffa8003e9eef064c0abbd77f309de733513da 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -156,10 +156,13 @@ Section fractional.
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
     FromSep P P1 P2.
   Proof. by rewrite /FromSep=>-[-> ->] [-> _] [-> _]. Qed.
-  Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
+  Global Instance combine_sep_fractional_bwd P P1 P2 Φ q1 q2 :
     AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → AsFractional P Φ (q1 + q2) →
-    FromSep P P1 P2 | 10.
-  Proof. by rewrite /FromSep=>-[-> _] [-> <-] [-> _]. Qed.
+    CombineSepAs P1 P2 P | 50.
+  (* Explicit cost, to make it easier to provide instances with higher or
+     lower cost. Higher-cost instances exist to combine (for example)
+     [l ↦{q1} v1] with [l ↦{q2} v2] where [v1] and [v2] are not unifiable. *)
+  Proof. by rewrite /CombineSepAs =>-[-> _] [-> <-] [-> _]. Qed.
 
   Global Instance from_sep_fractional_half_fwd P Q Φ q :
     AsFractional P Φ q → AsFractional Q Φ (q/2) →
@@ -167,8 +170,11 @@ Section fractional.
   Proof. by rewrite /FromSep -{1}(Qp.div_2 q)=>-[-> ->] [-> _]. Qed.
   Global Instance from_sep_fractional_half_bwd P Q Φ q :
     AsFractional P Φ (q/2) → AsFractional Q Φ q →
-    FromSep Q P P.
-  Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp.div_2. Qed.
+    CombineSepAs P P Q | 50.
+  (* Explicit cost, to make it easier to provide instances with higher or
+     lower cost. Higher-cost instances exist to combine (for example)
+     [l ↦{q1} v1] with [l ↦{q2} v2] where [v1] and [v2] are not unifiable. *)
+  Proof. rewrite /CombineSepAs=>-[-> <-] [-> _]. by rewrite Qp.div_2. Qed.
 
   Global Instance into_sep_fractional P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 267d8db8d4cc5e654e0d64abe9199d696f667445..bcfbfc14cea44e1fc5f1617233c34a1a7a6dda94 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -79,8 +79,8 @@ Proof.
   iMod (Hwp (OwnPGS _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
     first by rewrite /ownP; iFrame.
   iIntros "!> Hσ". iExists ∅. iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
-  iDestruct (own_valid_2 with "Hσ Hσf")
-    as %[Hp%Excl_included _]%auth_both_valid_discrete; simplify_eq; auto.
+  iCombine "Hσ Hσf"
+    gives %[Hp%Excl_included _]%auth_both_valid_discrete; simplify_eq; auto.
 Qed.
 
 
@@ -96,8 +96,8 @@ Section lifting.
     state_interp σ1 ns κs nt -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
   Proof.
     iIntros "Hσ● Hσ◯". rewrite /ownP.
-    by iDestruct (own_valid_2 with "Hσ● Hσ◯")
-      as %[->%Excl_included _]%auth_both_valid_discrete.
+    by iCombine "Hσ● Hσ◯"
+      gives %[->%Excl_included _]%auth_both_valid_discrete.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof.
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 205798085cd2f6c2ae5c5387a2149bb33108992b..7415815167b4558c1c9984dc490b68516b1476b8 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -689,6 +689,53 @@ Global Instance from_sep_big_sepMS_disj_union `{Countable A} (Φ : A → PROP) X
   FromSep ([∗ mset] y ∈ X1 ⊎ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
 Proof. by rewrite /FromSep big_sepMS_disj_union. Qed.
 
+(** MaybeCombineSepAs *)
+Global Instance maybe_combine_sep_as_affinely Q1 Q2 P progress :
+  MaybeCombineSepAs Q1 Q2 P progress →
+  MaybeCombineSepAs (<affine> Q1) (<affine> Q2) (<affine> P) progress | 30.
+Proof. rewrite /MaybeCombineSepAs =><-. by rewrite affinely_sep_2. Qed.
+Global Instance maybe_combine_sep_as_intuitionistically Q1 Q2 P progress :
+  MaybeCombineSepAs Q1 Q2 P progress →
+  MaybeCombineSepAs (â–¡ Q1) (â–¡ Q2) (â–¡ P) progress | 30.
+Proof. rewrite /MaybeCombineSepAs =><-. by rewrite intuitionistically_sep_2. Qed.
+Global Instance maybe_combine_sep_as_absorbingly Q1 Q2 P progress :
+  MaybeCombineSepAs Q1 Q2 P progress →
+  MaybeCombineSepAs (<absorb> Q1) (<absorb> Q2) (<absorb> P) progress | 30.
+Proof. rewrite /MaybeCombineSepAs =><-. by rewrite absorbingly_sep. Qed.
+Global Instance maybe_combine_sep_as_persistently Q1 Q2 P progress :
+  MaybeCombineSepAs Q1 Q2 P progress →
+  MaybeCombineSepAs (<pers> Q1) (<pers> Q2) (<pers> P) progress | 30.
+Proof. rewrite /MaybeCombineSepAs =><-. by rewrite persistently_sep_2. Qed.
+
+(** CombineSepGives *)
+(* The results of these recursive instances drop the input modalities. This is
+fine, because the [P] argument in [CombineSepGives Q1 Q2 P] is by definition
+beneath a [<pers>] modality, and we have:
+         - [<affine><pers> P ⊢ <pers> P] holds, we have
+              [<pers><affine> P ⊣⊢ <pers> P] by [persistently_affinely_elim]
+              and the obtained [â–¡ P] in [iCombine] is always [Affine] anyway.
+         - [â–¡ <pers> P = <affine><pers> <pers> P], see [<affine>] and [<pers>]
+         - [<absorb><pers> P ⊣⊢ <pers> P], see [absorbingly_elim_persistently]
+         - [<pers><pers> P ⊣⊢ <pers> P], see [persistently_idemp] *)
+Global Instance combine_sep_as_affinely Q1 Q2 P :
+  CombineSepGives Q1 Q2 P → CombineSepGives (<affine> Q1) (<affine> Q2) P | 30.
+Proof. by rewrite /CombineSepGives affinely_sep_2 affinely_elim => ->. Qed.
+Global Instance combine_sep_as_intuitionistically Q1 Q2 P :
+  CombineSepGives Q1 Q2 P → CombineSepGives (□ Q1) (□ Q2) P | 30.
+Proof. rewrite /CombineSepGives => <-. by rewrite !intuitionistically_elim. Qed.
+Global Instance combine_sep_as_absorbingly Q1 Q2 P :
+  CombineSepGives Q1 Q2 P → CombineSepGives (<absorb> Q1) (<absorb> Q2) P | 30.
+Proof.
+  rewrite /CombineSepGives -absorbingly_sep =>->.
+  by rewrite absorbingly_elim_persistently.
+Qed.
+Global Instance combine_sep_as_persistently Q1 Q2 P :
+  CombineSepGives Q1 Q2 P → CombineSepGives (<pers> Q1) (<pers> Q2) P | 30.
+Proof.
+  rewrite /CombineSepGives persistently_sep_2 => ->.
+  by rewrite persistently_idemp.
+Qed.
+
 (** IntoAnd *)
 Global Instance into_and_and p P Q : IntoAnd p (P ∧ Q) P Q | 10.
 Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
diff --git a/iris/proofmode/class_instances_embedding.v b/iris/proofmode/class_instances_embedding.v
index 67a609f543864ffb771b67914d99d4dc5bd81a0f..e013e24069bf117c7d4fa94dd888f48b3f428236 100644
--- a/iris/proofmode/class_instances_embedding.v
+++ b/iris/proofmode/class_instances_embedding.v
@@ -98,6 +98,16 @@ Global Instance from_sep_embed P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
 Proof. by rewrite /FromSep -embed_sep => <-. Qed.
 
+Global Instance maybe_combine_sep_as_embed Q1 Q2 P progress :
+  MaybeCombineSepAs Q1 Q2 P progress →
+  MaybeCombineSepAs ⎡Q1⎤ ⎡Q2⎤ ⎡P⎤ progress.
+Proof. by rewrite /MaybeCombineSepAs -embed_sep => <-. Qed.
+
+Global Instance combine_sep_gives_embed Q1 Q2 P :
+  CombineSepGives Q1 Q2 P →
+  CombineSepGives ⎡Q1⎤ ⎡Q2⎤ ⎡P⎤.
+Proof. by rewrite /CombineSepGives -embed_sep -embed_persistently => ->. Qed.
+
 Global Instance into_and_embed p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
 Proof.
diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
index c27ebf69d36e87fec03296b07bf929021a8b7bdc..6ee58f912c64b1c26450a6cb11e61ef0502ccbdc 100644
--- a/iris/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -76,6 +76,36 @@ Global Instance from_sep_except_0 P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /FromSep=><-. by rewrite except_0_sep. Qed.
 
+(** MaybeCombineSepAs *)
+Global Instance maybe_combine_sep_as_later Q1 Q2 P progress :
+  MaybeCombineSepAs Q1 Q2 P progress →
+  MaybeCombineSepAs (â–· Q1) (â–· Q2) (â–· P) progress.
+Proof. by rewrite /MaybeCombineSepAs -later_sep => <-. Qed.
+Global Instance maybe_combine_sep_as_laterN n Q1 Q2 P progress :
+  MaybeCombineSepAs Q1 Q2 P progress →
+  MaybeCombineSepAs (â–·^n Q1) (â–·^n Q2) (â–·^n P) progress.
+Proof. by rewrite /MaybeCombineSepAs -laterN_sep => <-. Qed.
+Global Instance maybe_combine_sep_as_except_0 Q1 Q2 P progress :
+  MaybeCombineSepAs Q1 Q2 P progress →
+  MaybeCombineSepAs (â—‡ Q1) (â—‡ Q2) (â—‡ P) progress.
+Proof. by rewrite /MaybeCombineSepAs -except_0_sep => <-. Qed.
+
+(** MaybeCombineSepGives *)
+Global Instance maybe_combine_sep_gives_later Q1 Q2 P :
+  CombineSepGives Q1 Q2 P →
+  CombineSepGives (â–· Q1) (â–· Q2) (â–· P).
+Proof. by rewrite /CombineSepGives -later_sep -later_persistently => ->. Qed.
+Global Instance maybe_combine_sep_gives_laterN n Q1 Q2 P :
+  CombineSepGives Q1 Q2 P →
+  CombineSepGives (â–·^n Q1) (â–·^n Q2) (â–·^n P).
+Proof. by rewrite /CombineSepGives -laterN_sep -laterN_persistently => ->. Qed.
+Global Instance maybe_combine_sep_gives_except_0 Q1 Q2 P :
+  CombineSepGives Q1 Q2 P →
+  CombineSepGives (â—‡ Q1) (â—‡ Q2) (â—‡ P).
+Proof.
+  by rewrite /CombineSepGives -except_0_sep -except_0_persistently => ->.
+Qed.
+
 (** IntoAnd *)
 Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 29a40387cfbe78074432952c74d9850db032845d..b76206de240513eb8585779ff276583a99cdab37 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -173,8 +173,7 @@ Global Hint Mode FromImpl + ! - - : typeclass_instances.
 Class FromSep {PROP : bi} (P Q1 Q2 : PROP) := from_sep : Q1 ∗ Q2 ⊢ P.
 Global Arguments FromSep {_} _%I _%I _%I : simpl never.
 Global Arguments from_sep {_} _%I _%I _%I {_}.
-Global Hint Mode FromSep + ! - - : typeclass_instances.
-Global Hint Mode FromSep + - ! ! : typeclass_instances. (* For iCombine *)
+Global Hint Mode FromSep + ! - - : typeclass_instances. (* For iSplit{L,R} *)
 
 Class FromAnd {PROP : bi} (P Q1 Q2 : PROP) := from_and : Q1 ∧ Q2 ⊢ P.
 Global Arguments FromAnd {_} _%I _%I _%I : simpl never.
@@ -247,6 +246,71 @@ Global Arguments IsExcept0 {_} _%I : simpl never.
 Global Arguments is_except_0 {_} _%I {_}.
 Global Hint Mode IsExcept0 + ! : typeclass_instances.
 
+(** [CombineSepAs], [MaybeCombineSepAs] and [CombineSepGives] are all used for
+  the [iCombine] tactic.
+
+These three classes take two hypotheses [P] and [Q] as input, and return a
+(possibly simplified) new hypothesis [R]. [CombineSepAs P Q R] means that [R]
+may be obtained by deleting both [P] and [Q], and that [R] is not a trivial
+combination. [MaybeCombineSepAs P Q R progress] is like [CombineSepAs], but
+[R] can be the trivial combination [P ∗ Q], and the [progress] parameter 
+indicates whether this trivial combination is used. [CombineSepGives P Q R] 
+means that [â–¡ R] may be obtained 'for free' from [P] and [Q]. The result [R] of 
+[CombineSepAs] and [MaybeCombineSepAs] will not contain the observations 
+from [CombineSepGives].
+
+We deliberately use separate typeclasses [CombineSepAs] and [CombineSepGives].
+This allows one to (1) combine hypotheses and get additional persistent
+information, (2) only combine the hypotheses, without the additional persistent
+information, (3) only get the additional persistent information, while keeping
+the original hypotheses. A possible alternative would have been something like
+[CombineSepAsGives P1 P2 P R := combine_as_gives : P1 ∗ P2 ⊢ P ∗ □ R],
+but this was deemed to be harder to use. Specifically, this would force you to
+always specify both [P] and [R], even though one might only have a good
+candidate for [P], but not [R], or the other way around.
+
+Note that [FromSep] and [CombineSepAs] have nearly the same definition. However,
+they have different Hint Modes and are used for different tactics. [FromSep] is
+used to compute the two new goals obtained after applying `iSplitL`/`iSplitR`,
+taking the current goal as input. [CombineSepAs] is used to combine two
+hypotheses into one. *)
+Class CombineSepAs {PROP : bi} (P Q R : PROP) := combine_sep_as : P ∗ Q ⊢ R.
+Global Arguments CombineSepAs {_} _%I _%I _%I : simpl never.
+Global Arguments combine_sep_as {_} _%I _%I _%I {_}.
+Global Hint Mode CombineSepAs + ! ! - : typeclass_instances.
+
+(** The [progress] parameter is of the following [progress_indicator] type: *)
+Inductive progress_indicator := MadeProgress | NoProgress.
+(** This aims to make [MaybeCombineSepAs] instances easier to read than if we
+had used Booleans. [NoProgress] indicates that the default instance
+[maybe_combine_sep_as_default] below has been used, while [MadeProgress]
+indicates that a [CombineSepAs] instance was used. *)
+Class MaybeCombineSepAs {PROP : bi}
+    (P Q R : PROP) (progress : progress_indicator) :=
+  maybe_combine_sep_as : P ∗ Q ⊢ R.
+Global Arguments MaybeCombineSepAs {_} _%I _%I _%I _ : simpl never.
+Global Arguments maybe_combine_sep_as {_} _%I _%I _%I _ {_}.
+Global Hint Mode MaybeCombineSepAs + ! ! - - : typeclass_instances.
+
+Global Instance maybe_combine_sep_as_combine_sep_as {PROP : bi} (R P Q : PROP) :
+  CombineSepAs P Q R → MaybeCombineSepAs P Q R MadeProgress | 20.
+Proof. done. Qed.
+
+Global Instance maybe_combine_sep_as_default {PROP : bi} (P Q : PROP) :
+  MaybeCombineSepAs P Q (P ∗ Q) NoProgress | 100.
+Proof. intros. by rewrite /MaybeCombineSepAs. Qed.
+
+(** We do not have this Maybe construction for [CombineSepGives], nor do we
+provide the trivial [CombineSepGives P Q True]. This is by design: when the user
+writes down a 'gives' clause in the [iCombine] tactic, they intend to receive
+non-trivial information. If such information cannot be found, we want to
+produce an error, instead of the trivial hypothesis [True]. *)
+Class CombineSepGives {PROP : bi} (P Q R : PROP) :=
+  combine_sep_gives : P ∗ Q ⊢ <pers> R.
+Global Arguments CombineSepGives {_} _%I _%I _%I : simpl never.
+Global Arguments combine_sep_gives {_} _%I _%I _%I {_}.
+Global Hint Mode CombineSepGives + ! ! - : typeclass_instances.
+
 (** The [ElimModal φ p p' P P' Q Q'] class is used by the [iMod] tactic.
 
 The inputs are [p], [P] and [Q], and the outputs are [φ], [p'], [P'] and [Q'].
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index ac576efcd33d238e458e8f992a96616defe0f8cf..4895c6b2788c8d0441e243d5408950104e37d2e8 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -1,5 +1,6 @@
 From iris.bi Require Export bi telescopes.
-From iris.proofmode Require Export base environments classes modality_instances.
+From iris.proofmode Require Export base environments classes classes_make
+                                   modality_instances.
 From iris.prelude Require Import options.
 Import bi.
 Import env_notations.
@@ -618,31 +619,168 @@ Proof.
   rewrite envs_split_sound //. by rewrite HQ1 HQ2.
 Qed.
 
-(** * Combining *)
-Class FromSeps {PROP : bi} (P : PROP) (Qs : list PROP) :=
-  from_seps : [∗] Qs ⊢ P.
-Local Arguments FromSeps {_} _%I _%I.
-Local Arguments from_seps {_} _%I _%I {_}.
-
-Global Instance from_seps_nil : @FromSeps PROP emp [].
-Proof. by rewrite /FromSeps. Qed.
-Global Instance from_seps_singleton P : FromSeps P [P] | 1.
-Proof. by rewrite /FromSeps /= right_id. Qed.
-Global Instance from_seps_cons P P' Q Qs :
-  FromSeps P' Qs → FromSep P Q P' → FromSeps P (Q :: Qs) | 2.
-Proof. by rewrite /FromSeps /FromSep /= => ->. Qed.
-
-Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
+(** * Combining
+For the [iCombine] tactic, users provide a [Ps : list PROP] which should be
+combined to a single [PROP]. The (public) classes currently available,
+[MaybeCombineSepAs] and [CombineSepGives], can combine two given [PROP]s. The
+following [CombineSepsAs] and [CombineSepsAsGives] typeclasses are an
+implementation detail of [iCombine], lifting the combining operation to
+one on [list PROP].
+
+Computing the 'gives' clause for a list of hypotheses is somewhat involved.
+We cannot just fold [CombineSepGives] over the list, since the output of the
+first [CombineSepGives] is not suitable as the input for the next iteration. For
+example, one might have [CombineSepGives (own γ a) (own γ b) (✓ (a ⋅ b))]. This
+does not directly allow us to combine [[own γ a; own γ b; own γ c]] to
+[✓ (a ⋅ b ⋅ c)], since [CombineSepGives (✓ (b ⋅ c)) (own γ a) ?] does not work.
+We need to first compute the 'as' clause of the tail to proceed: that is, use
+the fact that the 'as' clause of [[own γ b; own γ c]] is [own γ (b ⋅ c)].
+We could let [CombineSepsAs] compute the 'as' clause of the tail separately, but
+this results in quadratic complexity. We therefore bundle both clauses
+in the [CombineSepsAsGives] typeclass given below.
+
+Note that an alternative would be to compute pairwise 'gives' clauses of the
+head of the list with every element in the tail, and [∧]-ing that with the
+'gives' clause of the tail. In the example above, this would result in
+[✓ (a ⋅ b) ∧ ✓ (a ⋅ c) ∧ ✓ (b ⋅ c)]. This approach is not strong enough:
+it does not allow us to conclude [✓ (a ⋅ b ⋅ c)]. *)
+Class CombineSepsAsGives {PROP : bi} (Ps : list PROP) (Q R : PROP) := {
+  combine_seps_as_gives_as : [∗] Ps ⊢ Q;
+  combine_seps_as_gives_gives : [∗] Ps ⊢ <pers> R;
+}.
+Global Arguments CombineSepsAsGives {_} _%I _%I _%I.
+Global Arguments combine_seps_as_gives_as {_} _%I _%I _%I {_}.
+Global Arguments combine_seps_as_gives_gives {_} _%I _%I _%I {_}.
+(* FIXME: Hint Modes for this class are located after section closure due to
+Coq < 8.15 not supporting Global Hint Mode inside a section. Move them back
+once support for Coq < 8.15 is dropped *)
+
+Global Instance combine_seps_as_gives_nil : @CombineSepsAsGives PROP [] emp True.
+Proof.
+  split; first done. rewrite -persistently_True.
+  by apply pure_intro.
+Qed.
+Global Instance combine_seps_as_gives_singleton P :
+  CombineSepsAsGives [P] P True | 1.
+Proof.
+  split; first by rewrite /= right_id. rewrite -persistently_True.
+  by apply pure_intro.
+Qed.
+Global Instance combine_seps_gives_cons P Ps Q R Q' progress R' R'':
+  CombineSepsAsGives Ps Q R → (* [Q] and [R] are result from combining tail *)
+  MaybeCombineSepAs P Q Q' progress → (* [Q'] is [P] and [Q] combined *)
+  CombineSepGives P Q R' → (* [R'] is obtained for free from [P] and [Q] *)
+  MakeAnd R R' R'' → (* [R''] is nicely and-ing [R] and [R'] *)
+  CombineSepsAsGives (P :: Ps) Q' R'' | 2.
+(** By and-ing [R] and [R'], the resulting 'gives' clause [R''] will contain
+redundant information in some cases. However, this is necessary in other cases.
+
+For example, if we take [Ps = [own γ q1; own γ q2; own γ q3]] with [fracR] as
+the cmra, we get [R'' = (q2 + q3 ≤ 1) ∧ (q1 + q2 + q3 ≤ 1)]. Here, the first
+conjunct [R] follows from the second [R'], so there is redundancy.
+
+However, if we take
+[Ps = [own γ (CoPset E1); own γ (CoPset E2); own γ (CoPset E3)]] with
+[coPset_disjR] as the cmra, we get [R'' = (E2 ## E3) ∧ (E1 ## (E2 ∪ E3))], where
+the first conjunct does not follow from the second conjunct. Similarly for
+[Ps = [l ↦{q1} v1; l ↦{q2} v2; l ↦ {q3} v3]], where
+[R'' = (v1 = v2) ∧ (v2 = v3) ∧ {..other info about qs..}]. *)
+Proof.
+  case => HPsQ.
+  rewrite /CombineSepGives /MakeAnd => HPsR HQ' HR' HR''.
+  split; first by rewrite /= HPsQ HQ'.
+  rewrite -HR'' /=.
+  rewrite persistently_and. apply and_intro.
+  - by rewrite HPsR sep_elim_r.
+  - by rewrite HPsQ.
+Qed.
+
+(** If just the 'as' clause is needed, we will instead look for instances of
+the following [CombineSepsAs] typeclass. *)
+Class CombineSepsAs {PROP : bi} (Ps : list PROP) (Q : PROP) :=
+  combine_seps_as : [∗] Ps ⊢ Q.
+Global Arguments CombineSepsAs {_} _%I _%I.
+Global Arguments combine_seps_as {_} _%I _%I {_}.
+(* FIXME: Hint Modes for this class are located after section closure due to
+Coq < 8.15 not supporting Global Hint Mode inside a section. Move them back
+once support for Coq < 8.15 is dropped *)
+
+(** To ensure consistency of the output [Q] with that of [CombineSepsAsGives],
+the only instance of [CombineSepsAs] is constructed with an instance of
+[CombineSepsAsGives]. The one thing we need to keep in mind here is that
+instances of [CombineSepsAsGives] can only be found if [CombineSepGives]
+instances exist. Unlike for the 'as' clause, there is no trivial 'gives'
+combination --- if the user writes a 'gives' clause, they intend to receive
+non-trivial information, and should receive an error if this cannot be found.
+
+To still allow trivial combining with an 'as' clause, we add a trivial
+[CombineSepGives] instance _only_ during the typeclass search of [CombineSepsAs]
+via [CombineSepsAsGives]. This means we both get consistent output [Q] from
+[CombineSepsAsGives] and [CombineSepsAs], while [iCombine "H1 H2" gives "H"]
+still fails if "H1" and "H2" are unrelated *)
+Global Instance combine_seps_as_from_as_gives Ps Q R :
+  ((∀ P P', CombineSepGives P P' True%I) → CombineSepsAsGives Ps Q R) →
+  CombineSepsAs Ps Q.
+Proof.
+  move => HPsQ. apply HPsQ. move => P P'. rewrite /CombineSepGives.
+  rewrite -persistently_True. by apply pure_intro.
+Qed.
+
+Lemma tac_combine_as Δ1 Δ2 Δ3 js p Ps j P Q :
   envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) →
-  FromSeps P Ps →
+  CombineSepsAs Ps P →
   envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 →
   envs_entails Δ3 Q → envs_entails Δ1 Q.
 Proof.
   rewrite envs_entails_unseal => ??? <-. rewrite envs_lookup_delete_list_sound //.
-  rewrite from_seps. rewrite envs_app_singleton_sound //=.
+  rewrite combine_seps_as. rewrite envs_app_singleton_sound //=.
   by rewrite wand_elim_r.
 Qed.
 
+Lemma combine_seps_gives_of_envs Δ1 Δ2 js p Ps P R :
+  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) →
+  CombineSepsAsGives Ps P R →
+  of_envs Δ1 ⊢ of_envs Δ1 ∗ □ R.
+Proof.
+  move => ??.
+  assert (of_envs Δ1 ⊢ of_envs Δ1 ∧ <pers> R) as H.
+  { apply and_intro; first done.
+    rewrite envs_lookup_delete_list_sound //.
+    by rewrite combine_seps_as_gives_gives
+        intuitionistically_if_elim sep_elim_l. }
+  by rewrite {1}H persistently_and_intuitionistically_sep_r.
+Qed.
+
+Lemma tac_combine_gives Δ1 Δ2 Δ3 js p Ps j P Q R :
+  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) →
+  CombineSepsAsGives Ps P R →
+  envs_app true (Esnoc Enil j R) Δ1 = Some Δ3 →
+  envs_entails Δ3 Q → envs_entails Δ1 Q.
+Proof.
+  rewrite envs_entails_unseal => ??? <-.
+  erewrite combine_seps_gives_of_envs => //.
+  rewrite envs_app_singleton_sound //=.
+  by apply wand_elim_l'.
+Qed.
+
+Lemma tac_combine_as_gives Δ1 Δ2 Δ3 js p Ps j k P R Q :
+  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) →
+  CombineSepsAsGives Ps P R →
+    (* this â–¡ is okay, since we will call iDestructHyp anyway *)
+  envs_app p (Esnoc (Esnoc Enil j P) k (□ R)%I) Δ2 = Some Δ3 →
+  envs_entails Δ3 Q → envs_entails Δ1 Q.
+Proof.
+  rewrite envs_entails_unseal => ??? <-.
+  rewrite combine_seps_gives_of_envs //.
+  rewrite envs_lookup_delete_list_sound //.
+  rewrite combine_seps_as_gives_as envs_app_sound //.
+  destruct p => /=.
+  - rewrite right_id affinely_and -!intuitionistically_def.
+    rewrite intuitionistically_idemp and_sep_intuitionistically.
+    by rewrite -(comm _ (â–¡ R)%I) assoc wand_elim_r.
+  - by rewrite right_id -(comm _ (â–¡ R)%I) assoc wand_elim_r.
+Qed.
+
 (** * Conjunction/separating conjunction elimination *)
 Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) →
@@ -901,6 +1039,9 @@ Proof.
 Qed.
 End tactics.
 
+Global Hint Mode CombineSepsAs + ! - : typeclass_instances.
+Global Hint Mode CombineSepsAsGives + ! - - : typeclass_instances.
+
 (** * Introduction of modalities *)
 (** The following _private_ classes are used internally by [tac_modal_intro] /
 [iModIntro] to transform the proofmode environments when introducing a modality.
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 165482afdaab7c53e6a813563f34e95121542cb7..2b220023674af1c81c2e86d2ba4b6e2ca7415ca4 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1626,7 +1626,7 @@ Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let H := iFresh in
   let Δ := iGetCtx in
-  eapply tac_combine with _ _ Hs _ _ H _;
+  notypeclasses refine (tac_combine_as _ _ _ Hs _ _ H _ _ _ _ _ _);
     [pm_reflexivity ||
      let Hs := iMissingHypsCore Δ Hs in
      fail "iCombine: hypotheses" Hs "not found"
@@ -1634,11 +1634,81 @@ Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
     |pm_reflexivity ||
      let H := pretty_ident H in
      fail "iCombine:" H "not fresh"
+     (* should never happen in normal usage, since [H := iFresh]
+     FIXME: improve once consistent error messages are added,
+     see https://gitlab.mpi-sws.org/iris/iris/-/issues/499 *)
     |iDestructHyp H as pat].
 
 Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat) :=
   iCombine [H1;H2] as pat.
 
+Tactic Notation "iCombineGivesCore" constr(Hs) "gives" tactic3(tac) :=
+  let Hs := words Hs in
+  let Hs := eval vm_compute in (INamed <$> Hs) in
+  let H := iFresh in
+  let Δ := iGetCtx in
+  notypeclasses refine (tac_combine_gives _ _ _ Hs _ _ H _ _ _ _ _ _ _);
+    [pm_reflexivity ||
+     let Hs := iMissingHypsCore Δ Hs in
+     fail "iCombine: hypotheses" Hs "not found"
+    |tc_solve || fail "iCombine: cannot find 'gives' clause for hypotheses" Hs
+    |pm_reflexivity ||
+     let H := pretty_ident H in
+     fail "iCombine:" H "not fresh"
+     (* should never happen in normal usage, since [H := iFresh]
+     FIXME: improve once consistent error messages are added,
+     see https://gitlab.mpi-sws.org/iris/iris/-/issues/499 *)
+    |tac H].
+
+Tactic Notation "iCombine" constr(Hs) "gives" constr(pat) :=
+  iCombineGivesCore Hs gives (fun H => iDestructHyp H as pat).
+
+Tactic Notation "iCombine" constr(H1) constr(H2) "gives" constr(pat) :=
+  iCombine [H1;H2] gives pat.
+
+Tactic Notation "iCombine" constr(Hs) "gives" "%" simple_intropattern(pat) :=
+  iCombineGivesCore Hs gives (fun H => iPure H as pat).
+
+Tactic Notation "iCombine" constr(H1) constr(H2)
+                                      "gives" "%" simple_intropattern(pat) :=
+  iCombine [H1;H2] gives %pat.
+
+Tactic Notation "iCombineAsGivesCore" constr(Hs) "as" constr(pat1)
+                                      "gives" tactic3(tac) :=
+  let Hs := words Hs in
+  let Hs := eval vm_compute in (INamed <$> Hs) in
+  let H1 := iFresh in
+  let H2 := iFresh in
+  let Δ := iGetCtx in
+  notypeclasses refine (tac_combine_as_gives _ _ _ Hs _ _ H1 H2 _ _ _ _ _ _ _);
+    [pm_reflexivity ||
+     let Hs := iMissingHypsCore Δ Hs in
+     fail "iCombine: hypotheses" Hs "not found"
+    |tc_solve || fail "iCombine: cannot find 'gives' clause for hypotheses" Hs
+    |pm_reflexivity ||
+     let H1 := pretty_ident H1 in
+     let H2 := pretty_ident H2 in
+     fail "iCombine:" H1 "or" H2 "not fresh"
+     (* should never happen in normal usage, since [H1] and [H2] are [iFresh]
+     FIXME: improve once consistent error messages are added,
+     see https://gitlab.mpi-sws.org/iris/iris/-/issues/499 *)
+    |iDestructHyp H1 as pat1; tac H2].
+
+Tactic Notation "iCombine" constr(Hs) "as" constr(pat1) "gives" constr(pat2) :=
+  iCombineAsGivesCore Hs as pat1 gives (fun H => iDestructHyp H as pat2).
+
+Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat1)
+                                      "gives" constr(pat2) :=
+  iCombine [H1;H2] as pat1 gives pat2.
+
+Tactic Notation "iCombine" constr(Hs) "as" constr(pat1)
+                                      "gives" "%" simple_intropattern(pat2) :=
+  iCombineAsGivesCore Hs as pat1 gives (fun H => iPure H as pat2).
+
+Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat1)
+                                      "gives" "%" simple_intropattern(pat2) :=
+  iCombine [H1;H2] as pat1 gives %pat2.
+
 (** * Introduction tactic *)
 Ltac iIntros_go pats startproof :=
   lazymatch pats with
diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index cb6312aaccae86bea641bce0511a3d63ec5bb2f3..f32bd01b31f5b722ac6e557d49e0c8501a0cee78 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -55,8 +55,8 @@ Section mono_proof.
     wp_pures. wp_bind (CmpXchg _ _ _).
     iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
-    - iDestruct (own_valid_2 with "Hγ Hγf")
-        as %[?%max_nat_included _]%auth_both_valid_discrete.
+    - iCombine "Hγ Hγf"
+        gives %[?%max_nat_included _]%auth_both_valid_discrete.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply auth_update, (max_nat_local_update _ _ (MaxNat (S c))). simpl. auto. }
       wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
@@ -77,8 +77,8 @@ Section mono_proof.
     iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
     wp_load.
-    iDestruct (own_valid_2 with "Hγ Hγf")
-      as %[?%max_nat_included _]%auth_both_valid_discrete.
+    iCombine "Hγ Hγf"
+      gives %[?%max_nat_included _]%auth_both_valid_discrete.
     iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
     { apply auth_update, (max_nat_local_update _ _ (MaxNat c)); auto. }
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
@@ -152,7 +152,7 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
-    iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
+    iCombine "Hγ Hγf" gives % ?%frac_auth_included_total%nat_included.
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
   Qed.
@@ -163,7 +163,7 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
-    iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agree_L.
+    iCombine "Hγ Hγf" gives % <-%frac_auth_agree_L.
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     by iApply "HΦ".
   Qed.
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index 4b3912b054509c2bc60da5c497893b0859687dc7..c086cbe59781c4c1ec301ba3b5919222dfa882eb 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -50,7 +50,7 @@ Section tada.
     tada_lock_state γ s1 -∗ tada_lock_state γ s2 -∗ False.
   Proof.
     iIntros "[Hvar1 _] [Hvar2 _]".
-    iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[Hval _].
+    iCombine "Hvar1 Hvar2" gives %[Hval _].
     exfalso. done.
   Qed.
 
@@ -80,7 +80,7 @@ Section tada.
     wp_apply (l.(acquire_spec) with "Hislock").
     iIntros "[Hlocked Hvar1]".
     iMod "AU" as (s) "[[Hvar2 _] [_ Hclose]]".
-    iDestruct (ghost_var_agree with "Hvar1 Hvar2") as %<-.
+    iCombine "Hvar1 Hvar2" gives %[_ <-].
     iMod (ghost_var_update_2 Locked with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
     { rewrite Qp.quarter_three_quarter //. }
     iMod ("Hclose" with "[$Hvar2 $Hlocked $Hvar1]"); done.
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index 20780846b7837cc8cfd9729179bfd2a111605b7f..dfb8d277885782e5995ffa5f6c78c75775cb4164 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -72,7 +72,7 @@ Proof.
   - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
     + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
       wp_pures. by iApply "HΦ".
-    + iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
+    + iCombine "Hγ Hγ'" gives %[].
 Qed.
 End proof.
 
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index f0fe1f9049b27ef4d7b0248fce0a1c89f1d51edf..338c25acf2344e44152c94caa7f25a7f6a5d68e7 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -35,7 +35,7 @@ Section proof.
   Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
 
   Lemma locked_exclusive (γ : gname) : 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.
 
   Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
   Proof. solve_proper. Qed.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index ec8d4bdbc9ef804d9ddfacfc9b7d2520fbeec28a..7a42b151bb91758e20520a9fdd86147bdddcb447 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -68,7 +68,7 @@ Section proof.
   Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
   Proof.
     iIntros "[%σ1 H1] [%σ2 H2]".
-    iDestruct (own_valid_2 with "H1 H2") as %[[] _]%auth_frag_op_valid_1.
+    iCombine "H1 H2" gives %[[] _]%auth_frag_op_valid_1.
   Qed.
 
   Lemma is_lock_iff γ lk R1 R2 :
@@ -106,8 +106,8 @@ Section proof.
         { iNext. iExists o, n. iFrame. }
         wp_pures. case_bool_decide; [|done]. wp_if.
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
-      + iDestruct (own_valid_2 with "Ht Haown")
-          as %[_ ?%gset_disj_valid_op]%auth_frag_op_valid_1.
+      + iCombine "Ht Haown"
+          gives %[_ ?%gset_disj_valid_op]%auth_frag_op_valid_1.
         set_solver.
     - iModIntro. iSplitL "Hlo Hln Ha".
       { iNext. iExists o, n. by iFrame. }
@@ -152,17 +152,17 @@ Section proof.
     wp_lam. wp_proj. wp_bind (! _)%E.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
     wp_load.
-    iDestruct (own_valid_2 with "Hauth Hγo") as
+    iCombine "Hauth Hγo" gives
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
     iModIntro. iSplitL "Hlo Hln Hauth Haown".
     { iNext. iExists o, n. by iFrame. }
     wp_pures.
     iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
     iApply wp_fupd. wp_store.
-    iDestruct (own_valid_2 with "Hauth Hγo") as
+    iCombine "Hauth Hγo" gives
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
     iDestruct "Haown" as "[[Hγo' _]|Haown]".
-    { iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]%auth_frag_op_valid_1. }
+    { iCombine "Hγo Hγo'" gives %[[] ?]%auth_frag_op_valid_1. }
     iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
     { apply auth_update, prod_local_update_1.
       by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 6373e48be247877fa3ed76efd7ed11f0c1bd29bf..7cdf511dada746b1ad0f38a2899694444eed7094 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -206,17 +206,23 @@ Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝.
 Proof. apply mapsto_valid. Qed.
 Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
+Proof. iIntros "H1 H2". iCombine "H1 H2" gives %[? [=?]]. done. Qed.
+Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
+Proof. iIntros "H1 H2". iCombine "H1 H2" gives %[_ [=?]]. done. Qed.
+
+Global Instance mapsto_combine_sep_gives l dq1 dq2 v1 v2 : 
+  CombineSepGives (l ↦{dq1} v1) (l ↦{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝ | 20. 
+  (* We provide an instance with lower cost than the gen_heap instance
+     to avoid having to deal with Some v1 = Some v2 *)
 Proof.
-  iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [= ?]]. done.
+  rewrite /CombineSepGives. iIntros "[H1 H2]".
+  iCombine "H1 H2" gives %[? [=->]]. eauto.
 Qed.
-Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
-Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[= ?]. done. Qed.
 
 Lemma mapsto_combine l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
 Proof.
-  iIntros "Hl1 Hl2". iDestruct (mapsto_combine with "Hl1 Hl2") as "[$ Heq]".
-  by iDestruct "Heq" as %[= ->].
+  iIntros "Hl1 Hl2". by iCombine "Hl1 Hl2" as "$" gives %[_ ->].
 Qed.
 
 Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
diff --git a/iris_unstable/base_logic/mono_list.v b/iris_unstable/base_logic/mono_list.v
index f8db43cceb776c35172c9250ab9a3c9b51e3ea63..883f29e758880c0711327eb2390f82bcf1d77f20 100644
--- a/iris_unstable/base_logic/mono_list.v
+++ b/iris_unstable/base_logic/mono_list.v
@@ -88,7 +88,7 @@ Section mono_list_own.
     ⌜(q1 + q2 ≤ 1)%Qp ∧ l1 = l2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    by iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_auth_dfrac_op_valid_L.
+    by iCombine "H1 H2" gives %?%mono_list_auth_dfrac_op_valid_L.
   Qed.
   Lemma mono_list_auth_own_exclusive γ l1 l2 :
     mono_list_auth_own γ 1 l1 -∗ mono_list_auth_own γ 1 l2 -∗ False.
@@ -103,7 +103,7 @@ Section mono_list_own.
     ⌜ (q ≤ 1)%Qp ∧ l2 `prefix_of` l1 ⌝.
   Proof.
     unseal. iIntros "Hauth Hlb".
-    by iDestruct (own_valid_2 with "Hauth Hlb") as %?%mono_list_both_dfrac_valid_L.
+    by iCombine "Hauth Hlb" gives %?%mono_list_both_dfrac_valid_L.
   Qed.
 
   Lemma mono_list_lb_valid γ l1 l2 :
@@ -112,7 +112,7 @@ Section mono_list_own.
     ⌜ l1 `prefix_of` l2 ∨ l2 `prefix_of` l1 ⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    by iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_lb_op_valid_L.
+    by iCombine "H1 H2" gives %?%mono_list_lb_op_valid_L.
   Qed.
 
   Lemma mono_list_idx_agree γ i a1 a2 :
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 0ffa2e841437fb2951e4a2cd6919b4bd2369fc8f..bc4e313ff4cb7cbf185f6684ccf2eed186c7a12d 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -222,6 +222,27 @@ Tactic failure: wp_pure: "Hcred" is not fresh.
   WP ! #l [{ v, Φ v }]
 1 goal
   
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  l : loc
+  v1 : val
+  q1 : Qp
+  v2 : val
+  q2 : Qp
+  v3 : val
+  q3 : Qp
+  v4 : val
+  q4 : Qp
+  H : ((✓ (DfracOwn q3 ⋅ DfracOwn q4) ∧ v3 = v4)
+       ∧ ✓ (DfracOwn q2 ⋅ (DfracOwn q3 ⋅ DfracOwn q4)) ∧ v2 = v3)
+      ∧ ✓ (DfracOwn q1 ⋅ (DfracOwn q2 ⋅ (DfracOwn q3 ⋅ DfracOwn q4)))
+        ∧ v1 = v2
+  ============================
+  --------------------------------------∗
+  ⌜(q1 + (q2 + (q3 + q4)) ≤ 1)%Qp⌝ ∗ ⌜v1 = v2⌝ ∗ ⌜
+  v2 = v3⌝ ∗ ⌜v3 = v4⌝
+1 goal
+  
   Σ : gFunctors
   heapGS0 : heapGS Σ
   l : loc
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 023fbf3f74ad5e08ab1c46b2c3b62c65ff966a19..149c0c4ca507705593e020802c2d5f4f2719408c 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -408,6 +408,28 @@ Section mapsto_tests.
     l ↦{#q/2} v -∗ l ↦{#q/2} v -∗ l ↦{#q} v.
   Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.
 
+  Lemma mapsto_combine_2 l v1 q1 v2 q2 :
+    l ↦{#q1} v1 -∗ l ↦{#q2} v2 -∗
+    l ↦{#(q1 + q2)} v1 ∗ ⌜q1 + q2 ≤ 1⌝%Qp ∗ ⌜v1 = v2⌝.
+  Proof. iIntros "H1 H2". by iCombine "H1 H2" as "$" gives %[? ->]. Qed.
+
+  Lemma mapsto_combine_3 l v1 q1 v2 q2 v3 q3 :
+    l ↦{#q1} v1 -∗ l ↦{#q2} v2 -∗ l ↦{#q3} v3 -∗
+    l ↦{#(q1 + (q2 + q3))} v1 ∗ ⌜q1 + (q2 + q3) ≤ 1⌝%Qp ∗ ⌜v1 = v2⌝ ∗ ⌜v2 = v3⌝.
+  Proof.
+    iIntros "H1 H2 H3".
+    by iCombine "H1 H2 H3" as "$" gives %[[_ ->] [? ->]].
+  Qed.
+
+  Lemma mapsto_combine_4 l v1 q1 v2 q2 v3 q3 v4 q4 :
+    l ↦{#q1} v1 -∗ l ↦{#q2} v2 -∗ l ↦{#q3} v3 -∗ l ↦{#q4} v4 -∗
+    l ↦{#(q1 + (q2 + (q3 + q4)))} v1 ∗ ⌜q1 + (q2 + (q3 + q4)) ≤ 1⌝%Qp ∗
+      ⌜v1 = v2⌝ ∗ ⌜v2 = v3⌝ ∗ ⌜v3 = v4⌝.
+  Proof.
+    iIntros "H1 H2 H3 H4".
+    iCombine "H1 H2 H3 H4" as "$" gives %H. Show.
+    by destruct H as [[[_ ->] [_ ->]] [? ->]].
+  Qed.
 End mapsto_tests.
 
 Section inv_mapsto_tests.
diff --git a/tests/later_credits_paper.v b/tests/later_credits_paper.v
index a985a8c0c0ba2bddc60a762f8d11f9b38b1edc12..59d3e826ef3790180fa1d073e614363808dc708e 100644
--- a/tests/later_credits_paper.v
+++ b/tests/later_credits_paper.v
@@ -97,7 +97,7 @@ Proof.
   (** and use timelessness to strip the later over ["Hv'"].
      But we cannot do the same for ["Hinv'"], the knowledge about the nested invariant, because
      it is not timeless. And we also cannot take any program step to strip the later here! *)
-  iPoseProof (ghost_var_agree with "Hv Hv'") as "#<-".
+  iCombine "Hv Hv'" gives %[_ <-].
   (** Instead, we use the later credit to strip the later in front of the invariant.
     Here we make use of [lc_fupd_add_later], which adds a later to the goal using one credit,
     if the current goal is a fancy update. *)
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 378177ec1cac857a5ec8462674ea08494500dc5e..aae8557e32b8dae84a0c6b74d0160f24cb2143a8 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -90,9 +90,9 @@ Proof.
       subst; wp_match; [done|].
     wp_bind (! _)%E.
     iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
-    { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
+    { by iCombine "Hγ Hγ'" gives %?. }
     wp_load. Show.
-    iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_inv_L; subst.
+    iCombine "Hγ Hγ'" gives %?%to_agree_op_inv_L; subst.
     iModIntro. iSplitL "Hl".
     { iNext; iRight; by eauto. }
     wp_smart_apply wp_assert. wp_pures. by case_bool_decide.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 212e554eb1bdc8999ed90242968a10d962a2fdc2..a27781f02722a224457889a09f36d5622ff23c60 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -83,7 +83,7 @@ Proof.
       wp_cmpxchg_suc. iModIntro. iSplitR "HΦ".
       * iNext; iRight; iExists n; by iFrame.
       * wp_pures. iSplitR; first done. by iApply "HΦ".
-    + by iDestruct (own_valid_2 with "Hγ1 Hγ'") as %?.
+    + by iCombine "Hγ1 Hγ'" gives %?.
   - clear Φ. iIntros "!> %Φ _ HΦ /=". wp_lam. wp_bind (! _)%E.
     iInv N as ">Hγ".
     iAssert (∃ v, l ↦ v ∗ (⌜v = NONEV⌝ ∗ own γ (Pending (1/2)%Qp) ∨
@@ -110,9 +110,9 @@ Proof.
       wp_load; iModIntro; (iSplitL "Hl Hγ"; first by eauto with iFrame);
       wp_pures; by iApply "HΦ".
     + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
-      { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
+      { by iCombine "Hγ Hγ'" gives %?. }
       wp_load. Show.
-      iDestruct (own_valid_2 with "Hγ Hγ'") as %?%to_agree_op_inv_L; subst.
+      iCombine "Hγ Hγ'" gives %?%to_agree_op_inv_L; subst.
       iModIntro. iSplitL "Hl Hγ"; first by eauto with iFrame.
       wp_pures. iApply wp_assert. wp_op.
       iSplitR; first by case_bool_decide.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 9db702ed664dbb6e7b26b154098a31bd41accde3..6626c8ee2761d9689fa1159e598e68727e73a1e1 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -294,6 +294,14 @@ Tactic failure: iSpecialize: (|==> P)%I not persistent.
   ============================
   --------------------------------------∗
   ▷ (∃ _ : nat, True)
+"test_iCombine_nested_no_gives"
+     : string
+The command has indeed failed with message:
+Tactic failure: iCombine: cannot find 'gives' clause for hypotheses
+["HP"; "HQ"].
+The command has indeed failed with message:
+Tactic failure: iCombine: cannot find 'gives' clause for hypotheses
+["HP"; "HQ"].
 "test_iInduction_multiple_IHs"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index f53125f6efa65ddb17ec6c79a7df40e12165b99e..68f3c8cb6cdb23e2a84b72931bda6d122d0af62d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -750,6 +750,36 @@ Lemma test_iCombine_frame P Q R `{!Persistent R} :
   P -∗ Q -∗ R → R ∗ Q ∗ P ∗ R.
 Proof. iIntros "HP HQ #HR". iCombine "HQ HP HR" as "$". by iFrame. Qed.
 
+Check "test_iCombine_nested_no_gives".
+Lemma test_iCombine_nested_no_gives P Q :
+  <absorb><affine> P -∗ <absorb><affine> Q -∗ <absorb><affine> (P ∗ Q).
+Proof.
+  iIntros "HP HQ".
+  Fail iCombine "HP HQ" gives "Htriv".
+  Fail iCombine "HP HQ" as "HPQ" gives "Htriv".
+  iCombine "HP HQ" as "HPQ".
+  iExact "HPQ".
+Qed.
+
+Lemma test_iCombine_nested_gives1 P Q R :
+  CombineSepGives P Q R →
+  <absorb><affine> P -∗ <absorb><affine> Q -∗ <pers> R.
+Proof.
+  move => HPQR. iIntros "HP HQ".
+  iCombine "HP HQ" gives "#HR".
+  iExact "HR".
+Qed.
+
+Lemma test_iCombine_nested_gives2 n P Q R :
+  CombineSepGives P Q R →
+  ▷^n ◇ P -∗ ▷^n ◇ Q -∗ ▷^n ◇ (P ∗ Q) ∗ <pers> ▷^n ◇ R.
+Proof.
+  move => HPQR. iIntros "HP HQ".
+  iCombine "HP HQ" as "HPQ" gives "#HR".
+  iSplitL "HPQ"; first iExact "HPQ".
+  iExact "HR".
+Qed.
+
 Lemma test_iNext_evar P : P -∗ True.
 Proof.
   iIntros "HP". iAssert (▷ _ -∗ ▷ P)%I as "?"; last done.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index d7d70dce93dd295046fcd1294255408601e9d51b..9a9785e5768afcc21aeb646bef7029ad00283072 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -217,4 +217,12 @@ Section tests_iprop.
     ⎡ghost_var γ q a⎤ ⊢@{monPredI} ⎡ghost_var γ (q/2) a⎤ ∗ ⎡ghost_var γ (q/2) a⎤.
   Proof. iIntros "[$ $]". Qed.
 
+  Lemma test_embed_combine `{!ghost_varG Σ A} γ q (a1 a2 : A) :
+    ▷ ⎡ghost_var γ (q/2) a1⎤ ∗ ▷ ⎡ghost_var γ (q/2) a2⎤ ⊢@{monPredI}
+            ▷⎡ghost_var γ q a1⎤ ∗ ▷ ⌜a1 = a2⌝.
+  Proof.
+    iIntros "[H1 H2]".
+    iCombine "H1 H2" as "$" gives "#H". iNext.
+    by iDestruct "H" as %[_ ->].
+  Qed.
 End tests_iprop.