diff --git a/_CoqProject b/_CoqProject
index afa81b666197c4e2330c70067784274d3549a35f..042737916654109adb85083d63afd8a3b68ccec4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -85,12 +85,12 @@ iris/base_logic/upred.v
 iris/base_logic/bi.v
 iris/base_logic/derived.v
 iris/base_logic/proofmode.v
-iris/base_logic/proofmode_classes.v
-iris/base_logic/proofmode_instances.v
-iris/base_logic/validity_tactics.v
 iris/base_logic/base_logic.v
 iris/base_logic/algebra.v
 iris/base_logic/bupd_alt.v
+iris/base_logic/lib/proofmode_classes.v
+iris/base_logic/lib/proofmode_instances.v
+iris/base_logic/lib/validity_tactics.v
 iris/base_logic/lib/iprop.v
 iris/base_logic/lib/own.v
 iris/base_logic/lib/saved_prop.v
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 9772d47c735aaa16630471af6a9460d521c22ce9..93f32900e14574644c1342ecbf93e8d1c3a14368 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -46,7 +46,7 @@ Section proofs.
   Proof. split; [done|]. apply _. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
-  Proof. iIntros "H1 H2". by iCombineOwn "H1 H2" as "[H %]". Qed.
+  Proof. iIntros "H1 H2". by iCombineOwn "H1 H2" gives %H. Qed.
 
   Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
   Proof.
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 785acdf11a166180f824e0a386638bf899cf768f..d7f5361052fa4a3712292378c6a57d251d7c94bb 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -199,7 +199,7 @@ Section gen_heap.
     rewrite meta_token_eq /meta_token_def.
     iIntros "(%γm1 & #Hγm1 & Hm1) (%γm2 & #Hγm2 & Hm2)".
     iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
-    iCombineOwn ("Hm1 Hm2") as "[Hm %Hdisj]".
+    iCombineOwn ("Hm1 Hm2") as "Hm" gives %Hdisj.
     iExists _; iFrame "# ∗".
   Qed.
   Lemma meta_token_union l E1 E2 :
@@ -222,7 +222,7 @@ Section gen_heap.
     rewrite meta_eq /meta_def.
     iIntros "(%γm1 & Hγm1 & Hm1) (%γm2 & Hγm2 & Hm2)".
     iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
-    iCombineOwn ("Hm1 Hm2") as "[Hm %Henc]". naive_solver.
+    iCombineOwn ("Hm1 Hm2") gives %Henc. naive_solver.
   Qed.
   Lemma meta_set `{Countable A} E l (x : A) N :
     ↑ N ⊆ E → meta_token l E ==∗ meta l N x.
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index e305aeac9c00cd3f9c60eaedc8f0ffaf418dfa65..fcdc39d254e613b41bc1b12ba5b322615609ba74 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -138,9 +138,7 @@ Section inv_heap.
     ⌜∃ v I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
   Proof.
     iIntros "Hl_inv Hâ—¯".
-    iCombineOwn ("Hâ—¯ Hl_inv") as "%Hdest".
-    destruct Hdest as [[v' I'] [Hsome Hincl]].
-    apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & _ & HI & Hh).
+    iCombineOwn ("Hâ—¯ Hl_inv") gives %[[v' I'] [(v'' & I'' & _ & HI & Hh)%lookup_to_inv_heap_Some_2 Hincl]].
     move: Hincl; rewrite HI Some_included_total pair_included
       to_agree_included; intros [??]; eauto.
   Qed.
@@ -150,10 +148,8 @@ Section inv_heap.
     ⌜ ∃ I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
   Proof.
     iIntros "Hl_inv H●".
-    iCombineOwn ("H● Hl_inv") as "%Hdest".
-    destruct Hdest as [[v' I'] [Hsome Hincl]].
+    iCombineOwn ("H● Hl_inv") gives %[[v' I'] [(v'' & I'' & -> & HI & Hh)%lookup_to_inv_heap_Some_2 Hincl]].
     iPureIntro.
-    apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & -> & HI & Hh).
     move: Hincl; rewrite HI Some_included_total pair_included
       Excl_included to_agree_included; intros [-> ?]; eauto.
   Qed.
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index db2ef54ea7929347523f4803417d46a6a0b21355..27c3d83fab7b7a7ed5996a3434caaaedc93f4ed8 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -86,7 +86,7 @@ Section lemmas.
   Lemma ghost_map_elem_valid_2 k γ dq1 dq2 v1 v2 :
     k ↪[γ]{dq1} v1 -∗ k ↪[γ]{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
   Proof.
-    unseal. iIntros "H1 H2".
+    unseal. iIntros "H1 H2". (* cant use iCombineOwn here, since dq is abstract *)
     iDestruct (own_valid_2 with "H1 H2") as %?%gmap_view_frag_op_valid_L.
     done.
   Qed.
@@ -173,7 +173,7 @@ Section lemmas.
     ghost_map_auth γ q1 m1 -∗ ghost_map_auth γ q2 m2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ m1 = m2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    iCombineOwn "H1 H2" as "[Hm [%Hq %Hm]]". apply leibniz_equiv in Hm. subst. eauto.
+    by iCombineOwn "H1 H2" as "Hm" gives %[Hq ->%leibniz_equiv].
   Qed.
   Lemma ghost_map_auth_agree γ q1 q2 m1 m2 :
     ghost_map_auth γ q1 m1 -∗ ghost_map_auth γ q2 m2 -∗ ⌜m1 = m2⌝.
@@ -188,8 +188,7 @@ 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.
-    eauto.
+    by iCombineOwn "Hauth Hel" gives %?%leibniz_equiv.
   Qed.
 
   Lemma ghost_map_insert {γ m} k v :
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 0fc562e5cf4471fad731044cd3ab4daf65e56bc4..e889672788517bb856de0be1a7c0e8062030b1e2 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -53,8 +53,7 @@ Section lemmas.
     ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ a1 = a2⌝.
   Proof.
     unseal. iIntros "Hvar1 Hvar2".
-    iCombineOwn "Hvar1 Hvar2" as "[Hγ [%Hq %Ha]]".
-    apply leibniz_equiv in Ha as ->. eauto.
+    by iCombineOwn "Hvar1 Hvar2" gives %[Hq ->%leibniz_equiv].
   Qed.
   (** Almost all the time, this is all you really need. *)
   Lemma ghost_var_agree γ a1 q1 a2 q2 :
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 184e3ddcb9ea04229c0b36a893692553bfc1bd83..346803fcd0f342be2d3bb41dd0975d0b99153e3f 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -67,7 +67,7 @@ Section mono_nat.
     unseal. iIntros "H1 H2". Typeclasses Transparent mono_nat_auth.
     iDestruct "H1" as "[H1 H1']". (* this gets annoying because mono_nat_auth = ● _ ⋅ ◯ _ *)
     iDestruct "H2" as "[H2 H2']".
-    iCombineOwn "H1 H2" as "[H [%Hq %Hnm]]".
+    iCombineOwn "H1 H2" gives %[Hq Hnm].
     case: Hnm => ->. eauto.
   Qed.
   Lemma mono_nat_auth_own_exclusive γ n1 n2 :
@@ -81,8 +81,8 @@ 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 "Hauth" as "[Hauth Hauth2]".
-    iCombineOwn "Hauth Hlb" as "%Hn".
+    iDestruct "Hauth" as "[Hauth Hauth2]". Typeclasses Transparent mono_nat_lb.
+    iCombineOwn "Hauth Hlb" gives %Hn.
     rewrite own_valid auth_auth_dfrac_validI.
     iDestruct "Hauth" as "[%Hq _]". eauto.
   Qed.
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index 27e529d2428b9cfe51b1b4475abb71a7fd4ce528..28e430a44e2dca014734a7051202d51bdbaa9237 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -56,7 +56,7 @@ Section proofs.
   Proof. by apply own_alloc. Qed.
 
   Lemma na_own_disjoint p E1 E2 : na_own p E1 -∗ na_own p E2 -∗ ⌜E1 ## E2⌝.
-  Proof. iIntros "H1 H2". by iCombineOwn "H1 H2" as "[_ %HE]". Qed.
+  Proof. iIntros "H1 H2". by iCombineOwn "H1 H2" gives %HE. Qed.
 
   Lemma na_own_union p E1 E2 :
     E1 ## E2 → na_own p (E1 ∪ E2) ⊣⊢ na_own p E1 ∗ na_own p E2.
@@ -99,7 +99,7 @@ Section proofs.
     - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
       iIntros "!> [HP $]".
       iInv N as "[[_ >Hdis2]|>Hitok]".
-      + iCombineOwn "Hdis Hdis2" as "[Hdis %Hi]". set_solver.
+      + iCombineOwn "Hdis Hdis2" gives %Hi. set_solver.
       + iSplitR "Hitok"; last by iFrame. eauto with iFrame.
     - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
   Qed.
diff --git a/iris/base_logic/lib/proofmode_classes.v b/iris/base_logic/lib/proofmode_classes.v
new file mode 100644
index 0000000000000000000000000000000000000000..b37ef3b66f977c8ec6d6355be8ced4c9003cb93d
--- /dev/null
+++ b/iris/base_logic/lib/proofmode_classes.v
@@ -0,0 +1,66 @@
+From iris.algebra Require Import cmra.
+From iris.base_logic Require Import own.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
+
+
+(* Given two valid ghost elements a1 and a2, IsValidGives _ a1 a2 P computes 
+  a simplified proposition P that follows from the validity of a1 and a2 *)
+Class IsValidGives {A : cmra} M (a1 a2 : A) (P : uPred M) :=
+  is_valid_gives : ✓ (a1 ⋅ a2) ⊢ □ P.
+
+Global Hint Mode IsValidGives ! ! ! ! - : typeclass_instances.
+
+
+(* Often we can simplify a1 â‹… a2 to some new element a. This may make use
+  of validity, for example in the case of GSet. IsValidOp _ a a1 a2 P
+  says that a is a simplified element equivalent to a1 â‹… a2, and P 
+  a simplified proposition following from the validity of a1 and a2 *)
+Class IsValidOp {A : cmra} M (a a1 a2 : A) (P : uPred M) := {
+  is_valid_op_gives :> IsValidGives _ a1 a2 P ;
+  is_valid_op : ✓ (a1 ⋅ a2) ⊢@{uPredI M} a ≡ a1 ⋅ a2 ;
+}.
+
+Global Hint Mode IsValidOp ! ! - ! ! - : typeclass_instances.
+
+
+(* We are often interested in the consequences of ✓ (● _ ⋅ ◯ _).
+   We do not usually want to combine these elements, which is why we have
+   separated IsValidOp and IsValidGives. 
+   The consequence of ✓{n} (● a ⋅ ◯ b) in the model is that b ≼{n} a ∧ ✓{n} a. 
+   To cleanly reason about this in the logic, we provide notation for
+   the lifted version of ≼{n} *)
+
+Definition includedI {M : ucmra} {A : cmra} (a b : A) : uPred M
+  := (∃ c, b ≡ a ⋅ c)%I.
+
+Notation "a ≼ b" := (includedI a b) : bi_scope.
+
+
+(* IsIncluded _ a1 a2 P computes a simplified proposition P,
+   which is equivalent to a1 ≼ a2 if we assume ✓ a2. 
+   All we need is that P follows from a1 ≼ a2, but we use 
+   equivalence to ensure we are not forgetting any consequence *)
+
+Class IsIncluded {A : cmra} M (a1 a2 : A) (P : uPred M) := 
+  is_included_merge : ✓ a2 ⊢ a1 ≼ a2 ∗-∗ □ P.
+
+Global Hint Mode IsIncluded ! ! ! ! - : typeclass_instances.
+
+(* IsIncludedOrEq is used as a stepping stone to compute good
+   IsIncluded instances for unital extensions of non-unital cmra's.
+   For example, consider optionUR $ prodR fracR positiveR .
+   It includes IsIncludedM for efficiency's sake, to avoid computing it twice. *)
+Class IsIncludedOrEq {A : cmra} M (a1 a2 : A) (P_lt P_le : uPred M) := {
+  is_included_or_included : IsIncluded M a1 a2 P_lt;
+  is_included_or_eq_merge : ✓ a2 ⊢ (□ P_lt ∨ a1 ≡ a2) ∗-∗ □ P_le;
+}.
+
+Global Hint Mode IsIncludedOrEq ! ! ! ! - - : typeclass_instances.
+
+(* HasRightId a is also used to compute good IsIncluded instances.
+   Note that this is weaker than having a unit! Consider min_natR, agreeR *)
+Class HasRightId {A : cmra} (a : A) :=
+  has_right_id : a ≼ a.
+
+Global Hint Mode HasRightId ! ! : typeclass_instances.
\ No newline at end of file
diff --git a/iris/base_logic/proofmode_instances.v b/iris/base_logic/lib/proofmode_instances.v
similarity index 85%
rename from iris/base_logic/proofmode_instances.v
rename to iris/base_logic/lib/proofmode_instances.v
index 02d4b357bc11137f00b793a2334c4e2ac1b78403..bb74114c362c481a6c26d85b6c62a6d0832e6cd9 100644
--- a/iris/base_logic/proofmode_instances.v
+++ b/iris/base_logic/lib/proofmode_instances.v
@@ -1,11 +1,105 @@
 From iris.algebra Require Import cmra proofmode_classes.
 From iris.proofmode Require Import proofmode.
-From iris.base_logic Require Import own proofmode_classes.
+From iris.base_logic.lib Require Import own proofmode_classes.
 From iris.prelude Require Import options.
 
 Set Default Proof Using "Type".
 
 
+Section proper.
+  Context {M : ucmra} {A : cmra}.
+  Implicit Types a : A.
+
+  Global Instance includedI_proper_1 : 
+    NonExpansive2 (includedI (M := M) (A := A)).
+  Proof. solve_proper. Qed.
+  Global Instance includedI_proper_2 : 
+    Proper ((≡) ==> (≡) ==> (≡)) (includedI (M := M) (A := A)).
+  Proof. solve_proper. Qed.
+
+  Global Instance is_valid_gives_proper :
+    Proper ((≡) ==> (≡) ==> (=) ==> (iff)) (IsValidGives (A := A) M).
+  Proof. solve_proper. Qed.
+  Lemma is_valid_gives_weaken a1 a2 P1 P2 :
+    IsValidGives M a1 a2 P1 →
+    (✓ (a1 ⋅ a2) ∗ □ P1 ⊢ P2) →
+    IsValidGives M a1 a2 P2.
+  Proof.
+    rewrite /IsValidGives => HP HP1P2.
+    iIntros "#H✓".
+    rewrite -HP1P2.
+    iFrame "#". by rewrite -HP.
+  Qed.
+  Lemma is_valid_gives_true a1 a2 : IsValidGives M a1 a2 True.
+  Proof. rewrite /IsValidGives; eauto. Qed.
+
+  Global Instance is_valid_op_proper :
+    Proper ((≡) ==> (≡) ==> (≡) ==> (=) ==> (iff)) (IsValidOp (A := A) M).
+  Proof.
+    move => a1 a1' Ha1 a2 a2' Ha2 a a' Ha P2' P2 ->.
+    split; case => H1 H2; split.
+    - by eapply is_valid_gives_proper.
+    - rewrite -Ha -Ha2 -Ha1 //.
+    - by eapply is_valid_gives_proper.
+    - rewrite Ha2 Ha Ha1 //.
+  Qed.
+  Lemma is_valid_op_weaken a a1 a2 P1 P2 :
+    IsValidOp M a a1 a2 P1 →
+    (✓ (a1 ⋅ a2) ∗ □ P1 ⊢ P2) →
+    IsValidOp M a a1 a2 P2.
+  Proof.
+    case => HP Ha HP1P2; split; last done.
+    by eapply is_valid_gives_weaken.
+  Qed.
+
+  Global Instance is_included_proper : 
+    Proper ((≡) ==> (≡) ==> (≡) ==> (iff)) (IsIncluded (A := A) M).
+  Proof. solve_proper. Qed.
+  Lemma is_included_weaken a1 a2 P1 P2 :
+    IsIncluded M a1 a2 P1 →
+    (✓ a2 ⊢ □ P1 ∗-∗ □ P2) →
+    IsIncluded M a1 a2 P2.
+  Proof.
+    rewrite /IsIncluded => HP1a HP1P2.
+    iIntros "#H✓". iApply bi.wand_iff_trans.
+    - by iApply HP1a.
+    - by iApply HP1P2.
+  Qed.
+
+  Global Instance is_included_or_eq_proper : 
+    Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (iff)) (IsIncludedOrEq (A := A) M).
+  Proof.
+    move => a1 a1' Ha1 a2 a2' Ha2 P1' P1 HP1 P2' P2 HP2.
+    split; case => H1 H2; split.
+    - revert H1; apply is_included_proper => //.
+    - rewrite -Ha2 -Ha1 -HP1 -HP2 //.
+    - revert H1; apply is_included_proper => //.
+    - rewrite Ha2 Ha1 HP1 HP2 //.
+  Qed.
+  Lemma is_included_or_eq_weaken a1 a2 P1 P2 P3 P4 :
+    IsIncludedOrEq M a1 a2 P1 P2 →
+    (✓ a2 ⊢ □ P1 ∗-∗ □ P3) →
+    (✓ a2 ⊢ □ P2 ∗-∗ □ P4) →
+    IsIncludedOrEq M a1 a2 P3 P4.
+  Proof.
+    case => HP1 HP1P2 HP1P3 HP2P4; split; first by eapply is_included_weaken.
+    iIntros "#H✓". 
+    iApply bi.wand_iff_trans; last by iApply HP2P4.
+    iApply bi.wand_iff_trans; last by iApply HP1P2.
+    iSplit; iIntros "[#HP|$]"; iLeft; by iApply HP1P3.
+  Qed.
+
+  Global Instance valid_gives_emp_valid a1 a2 P:
+    AsEmpValid (IsValidGives M a1 a2 P) (✓ (a1 ⋅ a2) -∗ □ P).
+  Proof.
+    rewrite /AsEmpValid /IsValidGives. split;
+    iIntros (HP) "H✓"; by iApply HP.
+  Qed.
+End proper.
+
+Global Hint Immediate is_valid_gives_true : core.
+
+
 Global Instance includedI_into_pure `{CmraDiscrete A} (a b : A) {M} : 
   IntoPure (PROP := uPredI M) (a ≼ b)%I (a ≼ b).
 Proof.
@@ -23,9 +117,13 @@ Section cmra_instances.
     IsOp a a1 a2 → IsValidOp M a a1 a2 True.
   Proof. rewrite /IsOp => H; split; [ | rewrite H]; eauto. Qed.
 
+  Lemma is_valid_gives_comm a1 a2 P :
+    IsValidGives M a1 a2 P → IsValidGives M a2 a1 P.
+  Proof. rewrite /IsValidGives comm //. Qed.
+
   Lemma is_valid_op_comm a a1 a2 P :
     IsValidOp M a a1 a2 P → IsValidOp M a a2 a1 P.
-  Proof. case; split; rewrite comm //. Qed.
+  Proof. case; split; rewrite /IsValidGives comm //. Qed.
 
   Lemma is_included_merge' a1 a2 P :
     IsIncluded M a1 a2 P →
@@ -175,14 +273,14 @@ Section numbers.
     IsValidOp M q q1 q2 Pq → IsValidOp M (DfracOwn q) (DfracOwn q1) (DfracOwn q2) Pq.
   Proof.
     move => [H1 H2]; split.
-    - rewrite /op /cmra_op /=. rewrite dfrac_validI -frac_validI //.
+    - rewrite /op /cmra_op /= /IsValidGives dfrac_validI /= -frac_validI //.
     - rewrite /op /cmra_op /= dfrac_validI -frac_validI H2.
       iIntros "->" => //.
   Qed.
 
   Global Instance dfrac_valid_op_with_discarded_r (q : Qp) :
     IsValidOp M (DfracOwn q ⋅ DfracDiscarded) (DfracOwn q) DfracDiscarded ⌜(q < 1)%Qp⌝.
-  Proof. split; [rewrite dfrac_validI | ]; eauto. Qed.
+  Proof. split; [rewrite /IsValidGives dfrac_validI | ]; eauto. Qed.
 
   Global Instance dfrac_valid_op_with_discarded_l (q : Qp) :
     IsValidOp M (DfracOwn q ⋅ DfracDiscarded) DfracDiscarded (DfracOwn q) ⌜(q < 1)%Qp⌝.
@@ -342,7 +440,7 @@ Section optional.
 
   Global Instance option_some_valid_op a a1 a2 P :
     IsValidOp M a a1 a2 P → IsValidOp M (Some a) (Some a1) (Some a2) P.
-  Proof. case => HP Ha. split; rewrite -Some_op option_validI // Ha option_equivI //. Qed.
+  Proof. case => HP Ha. split; rewrite /IsValidGives -Some_op option_validI // Ha option_equivI //. Qed.
   Global Instance option_included_merge a1 a2 P1 P2 :
     IsIncludedOrEq M a1 a2 P1 P2 →
     IsIncluded M (Some a1) (Some a2) P2 | 100.
@@ -392,7 +490,7 @@ Section csum.
     IsValidOp _ (Cinl a) (Cinl (B := B) a1) (Cinl (B := B) a2) P.
   Proof.
     case => HP Ha. 
-    split; rewrite -Cinl_op csum_validI // Ha.
+    split; rewrite /IsValidGives -Cinl_op csum_validI // Ha.
     iIntros "Ha".
     by iRewrite "Ha".
   Qed.
@@ -401,16 +499,16 @@ Section csum.
     IsValidOp _ (Cinr b) (Cinr (A := A) b1) (Cinr (A := A) b2) P.
   Proof.
     case => HP Ha. 
-    split; rewrite -Cinr_op csum_validI // Ha.
+    split; rewrite /IsValidGives -Cinr_op csum_validI // Ha.
     iIntros "Ha".
     by iRewrite "Ha".
   Qed.
   Global Instance sum_inl_inr_invalid_op a b :
     IsValidOp M (CsumBot) (Cinl (B := B) a) (Cinr (A := A) b) False.
-  Proof. split; rewrite /op /= /cmra_op /= csum_validI; eauto. Qed.
+  Proof. split; rewrite /IsValidGives /op /= /cmra_op /= csum_validI; eauto. Qed.
   Global Instance sum_inr_inl_invalid_op a b :
     IsValidOp M (CsumBot) (Cinr (A := B) a) (Cinl (B := A) b) False.
-  Proof. split; rewrite /op /= /cmra_op /= csum_validI; eauto. Qed.
+  Proof. split; rewrite /IsValidGives /op /= /cmra_op /= csum_validI; eauto. Qed.
   Global Instance sum_inl_included_merge a1 a2 P :
     IsIncluded _ a1 a2 P →
     IsIncluded _ (Cinl (B := B) a1) (Cinl (B := B) a2) P | 100.
@@ -506,8 +604,8 @@ Section prod.
     MakeAnd P1 P2 P →
     IsValidOp _ (x, y) (x1, y1) (x2, y2) P.
   Proof.
-    rewrite /MakeAnd => Hxs Hys HP. split; rewrite -pair_op prod_validI /=.
-    - rewrite !is_valid_merge -HP bi.intuitionistically_and //.
+    rewrite /MakeAnd => Hxs Hys HP. split; rewrite /IsValidGives -pair_op prod_validI /=.
+    - rewrite !is_valid_op_gives -HP bi.intuitionistically_and //.
     - rewrite prod_equivI /= !is_valid_op //.
   Qed.
 
@@ -632,7 +730,7 @@ Section excl.
 
   Global Instance excl_valid_op e1 e2 :
     IsValidOp M ExclBot e1 e2 False.
-  Proof. split; rewrite excl_validI /=; eauto. Qed.
+  Proof. split; rewrite /IsValidGives excl_validI /=; eauto. Qed.
   Global Instance excl_included_merge e1 e2 :
     IsIncluded M e1 e2 False.
   Proof.
@@ -661,7 +759,7 @@ Section agree.
   Global Instance agree_valid_op o1 o2 :
     IsValidOp M (to_agree o1) (to_agree o1) (to_agree o2) (o1 ≡ o2)%I.
   Proof.
-    split; rewrite agree_validI agree_equivI; first eauto.
+    split; rewrite /IsValidGives agree_validI agree_equivI; first eauto.
     iIntros "H".
     iRewrite "H".
     by rewrite agree_idemp.
@@ -788,9 +886,9 @@ Section reservation_map.
   Global Instance combine_reservation_token E1 E2 :
     IsValidOp M (reservation_map_token (A := A) (E1 ∪ E2)) (reservation_map_token E1) (reservation_map_token E2) ⌜E1 ## E2⌝.
   Proof.
-    split.
-    - rewrite reservation_op reservation_validI /= !is_valid_merge. iIntros "[_ #$]".
-    - rewrite reservation_op reservation_validI /= !is_valid_merge. iIntros "[_ %]".
+    split; rewrite /IsValidGives reservation_op reservation_validI /= !is_valid_op_gives.
+    - iIntros "[_ #$]".
+    - iIntros "[_ %]".
       rewrite reservation_map_token_union //.
   Qed.
 
@@ -808,8 +906,8 @@ Section reservation_map.
     IsValidOp _ b b1 b2 P →
     IsValidOp _ (reservation_map_data k b) (reservation_map_data k b1) (reservation_map_data k b2) P.
   Proof.
-    split; rewrite -reservation_map_data_op reservation_map_data_validI.
-    - rewrite is_valid_merge //.
+    split; rewrite /IsValidGives -reservation_map_data_op reservation_map_data_validI.
+    - rewrite is_valid_gives //.
     - rewrite is_valid_op.
       iIntros "Heq".
       by iRewrite "Heq".
@@ -924,7 +1022,7 @@ Section view.
     IsValidOp M (view_frag (rel := rel) b) (◯V b1) (◯V b2) (∃ a, rel_holds_for a b).
   Proof.
     rewrite /IsOp => Hb; split.
-    - rewrite -view_frag_op view_validI /=.
+    - rewrite /IsValidGives -view_frag_op view_validI /=.
       iDestruct 1 as "[_ [%a #Ha]]". rewrite -Hb. eauto.
     - rewrite Hb view_frag_op. eauto.
   Qed.
@@ -951,7 +1049,7 @@ Section view.
     IsValidOp M (view_auth (rel := rel) dq a1) (●V{dq1} a1) (●V{dq2} a2) (Pq ∧ a1 ≡ a2 ∧ rel_holds_for a2 ε)%I.
   Proof.
     move => Hq; split.
-    - rewrite view_auth_dfrac_op_validI is_valid_merge.
+    - rewrite /IsValidGives view_auth_dfrac_op_validI is_valid_gives.
       iIntros "(#$ & #$ & #$)".
     - rewrite view_auth_dfrac_op_validI is_valid_op.
       iIntros "(-> & Heq & _)".
@@ -977,8 +1075,8 @@ Section auth.
     IsValidOp M a a1 a2 P →
     IsValidOp M (â—¯ a) (â—¯ a1) (â—¯ a2) P.
   Proof.
-    move => HPa. split; rewrite -auth_frag_op auth_frag_validI //.
-    - rewrite is_valid_merge //.
+    move => HPa. split; rewrite /IsValidGives -auth_frag_op auth_frag_validI //.
+    - rewrite is_valid_gives //.
     - rewrite is_valid_op.
       iIntros "H".
       by iRewrite "H".
@@ -1000,6 +1098,20 @@ Section auth.
     - rewrite /auth_auth. iSolveTC. 
     - iIntros "[_ #($ & $ & _)]".
   Qed.
+
+  (* We do not provide IsValidOp for combinations of ● and ◯: instead, we provide IsValidGives *)
+  Global Instance auth_frag_is_valid_gives dq a1 a2 P :
+    IsIncluded M a2 a1 P →
+    IsValidGives _ (●{dq} a1) (◯ a2) P.
+  Proof.
+    rewrite /IsIncluded /IsValidGives auth_both_dfrac_validI => HP.
+    iIntros "(% & #Hle & #Ha)".
+    by iApply HP.
+  Qed.
+  Global Instance auth_frag_is_valid_gives_swap dq a1 a2 P :
+    IsIncluded M a2 a1 P →
+    IsValidGives _ (◯ a2) (●{dq} a1) P.
+  Proof. intros; eapply is_valid_gives_comm, _. Qed.
 End auth.
 
 
@@ -1020,6 +1132,15 @@ Section frac_auth.
     apply auth_frag_valid_op, option_some_valid_op.
     by eapply prod_valid_op.
   Qed.
+
+  Global Instance frac_auth_frag_is_valid_gives q a1 a2 P :
+    IsIncluded M (Some (q, a2)) (Some (1%Qp, a1)) P →
+    IsValidGives _ (●F a1) (◯F{q} a2) P.
+  Proof. eapply auth_frag_is_valid_gives. Qed.
+  Global Instance frac_auth_frag_is_valid_gives_swap q a1 a2 P :
+    IsIncluded M (Some (q, a2)) (Some (1%Qp, a1)) P →
+    IsValidGives _ (◯F{q} a2) (●F a1) P.
+  Proof. intros; eapply is_valid_gives_comm, _. Qed.
 End frac_auth.
 
 
@@ -1035,6 +1156,15 @@ Section excl_auth.
     IsValidOp M (Some ea) (Excl' a1) (Excl' a2) P →
     IsValidOp M (â—¯ (Some ea)) (â—¯E a1) (â—¯E a2) P.
   Proof. apply auth_frag_valid_op. Qed.
+
+  Global Instance excl_auth_frag_is_valid_gives a1 a2 P :
+    IsIncluded M (Excl' a2) (Excl' a1) P →
+    IsValidGives _ (●E a1) (◯E a2) P.
+  Proof. eapply auth_frag_is_valid_gives. Qed.
+  Global Instance excl_auth_frag_is_valid_gives_swap a1 a2 P :
+    IsIncluded M (Excl' a2) (Excl' a1) P →
+    IsValidGives _ (◯E a2) (●E a1) P.
+  Proof. intros; eapply is_valid_gives_comm, _. Qed.
 End excl_auth.
 
 
@@ -1104,11 +1234,11 @@ Section gmap_view.
     IsValidOp _ (gmap_view_frag k dq v1) (gmap_view_frag k dq1 v1) (gmap_view_frag k dq2 v2) (P ∧ v1 ≡ v2).
   Proof.
     move => H0; split.
-    - rewrite view_validI /=.
+    - rewrite /IsValidGives view_validI /=.
       iDestruct 1 as "[_ [%m Hm]]".
       rewrite singleton_op -pair_op gmap_view_rel_holds_singleton /=.
       iDestruct "Hm" as "[%v3 (#Hv3 & Hv3' & _)]".
-      rewrite to_agree_op_simple is_valid_merge bi.and_elim_l agree_equivI bi.intuitionistically_and.
+      rewrite to_agree_op_simple is_valid_gives bi.and_elim_l agree_equivI bi.intuitionistically_and.
       eauto.
     - rewrite view_validI /=.
       iDestruct 1 as "[_ [%m Hm]]".
@@ -1127,5 +1257,15 @@ Section gmap_view.
     - iIntros "(_ & #$ & #$ & _ )".
   Qed.
 
+  Global Instance gmap_view_auth_frag_gives dq1 m k dq2 v :
+    IsValidGives M (gmap_view_auth dq1 m) (gmap_view_frag k dq2 v) (m !! k ≡ Some v).
+  Proof.
+    rewrite /IsValidGives view_validI /=.
+    iDestruct 1 as (m') "(Hm' & _ & Hr & _)".
+    iRevert "Hr". rewrite agree_equivI. iRewrite -"Hm'". clear m'.
+    rewrite left_id gmap_view_rel_holds_singleton.
+    iDestruct 1 as (v') "(Hv1 & Hv2 & ->)". simpl.
+    rewrite agree_equivI. by iRewrite "Hv1".
+  Qed.
 End gmap_view.
 
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 466119f8ac38f6e3945ef3748d6663d2adb6ad3f..e4a49cf1d6321b3838244dd5501736f9e3dfcfc7 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -56,7 +56,7 @@ Section saved_anything.
     saved_anything_own γ x -∗ saved_anything_own γ y -∗ x ≡ y.
   Proof.
     iIntros "Hx Hy". rewrite /saved_anything_own.
-    iCombineOwn "Hx Hy" as "[H #$]".
+    iCombineOwn "Hx Hy" gives "#$".
   Qed.
 End saved_anything.
 
diff --git a/iris/base_logic/lib/validity_tactics.v b/iris/base_logic/lib/validity_tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..7579fc2340f3775d692a69899c7d33ac20ed48b0
--- /dev/null
+++ b/iris/base_logic/lib/validity_tactics.v
@@ -0,0 +1,155 @@
+From iris.algebra Require Import cmra proofmode_classes auth frac_auth.
+From iris.proofmode Require Import proofmode environments.
+From iris.base_logic.lib Require Import own proofmode_classes proofmode_instances.
+From iris.prelude Require Import options.
+
+(* base lemmas to use the validity typeclasses *)
+
+Lemma own_valid_op {A : cmra} (a a1 a2 : A) γ `{!inG Σ A} (P : iProp Σ) :
+  IsValidOp _ a a1 a2 P →
+  own γ a1 -∗ own γ a2 -∗ own γ a ∗ □ P.
+Proof.
+  case => HP Ha.
+  iIntros "Ha1 Ha2".
+  iAssert (✓ (a1 ⋅ a2))%I as "#H✓".
+  { iApply (own_valid_2 with "Ha1 Ha2"). }
+  iSplit; last by iApply HP.
+  iAssert (a ≡ a1 ⋅ a2)%I with "[Ha1 Ha2]" as "#Heq"; first by iApply Ha.
+  iRewrite "Heq".
+  rewrite own_op; iFrame.
+Qed.
+
+Lemma own_valid_gives {A : cmra} (a1 a2 : A) γ `{!inG Σ A} (P : iProp Σ) :
+  IsValidGives _ a1 a2 P →
+  own γ a1 -∗ own γ a2 -∗ □ P.
+Proof.
+  rewrite /IsValidGives => HaP.
+  rewrite own_valid_2. apply bi.wand_intro_r.
+  by erewrite bi.wand_elim_l.
+Qed.
+
+
+(* now their coq tactic variants, for applying them to IPM proofs *)
+
+Lemma tac_own_valid_op i1 i2 {A : cmra} (a a1 a2 : A) p1 p2 γ `{!inG Σ A} (P G : iProp Σ) Δ :
+  envs_lookup i1 Δ = Some (p1, own γ a1) →
+  envs_lookup i2 (envs_delete true i1 p1 Δ) = Some (p2, own γ a2) →
+  IsValidOp _ a a1 a2 P →
+  envs_entails (envs_delete true i2 p2 (envs_delete true i1 p1 Δ)) (own γ a -∗ P -∗ G)%I →
+  envs_entails Δ G.
+Proof.
+  rewrite envs_entails_eq => Hi1 Hi2 HaP HΔ.
+  erewrite envs_lookup_sound => //.
+  erewrite envs_lookup_sound => //.
+  rewrite !bi.intuitionistically_if_elim HΔ.
+  iIntros "(Ha1 & Ha2 & HaPG)".
+  iDestruct (own_valid_2 with "Ha1 Ha2") as "#H✓".
+  iApply ("HaPG" with "[Ha1 Ha2]").
+  - case: HaP => _ HaP.
+    rewrite HaP.
+    iRewrite "H✓".
+    by iCombine "Ha1 Ha2" as "$".
+  - rewrite is_valid_gives //.
+Qed.
+
+Lemma tac_own_valid_gives i1 i2 {A : cmra} (a1 a2 : A) p1 p2 γ `{!inG Σ A} (P G : iProp Σ) Δ :
+  envs_lookup i1 Δ = Some (p1, own γ a1) →
+  envs_lookup i2 (envs_delete true i1 p1 Δ) = Some (p2, own γ a2) →
+  IsValidGives _ a1 a2 P →
+  envs_entails Δ (□ P -∗ G)%I →
+  envs_entails Δ G.
+Proof.
+  rewrite envs_entails_eq => Hi1 Hi2 HaP HΔ.
+  iIntros "HΔ".
+  iAssert (â–¡ P)%I as "#HP".
+  { erewrite envs_lookup_sound => //.
+    erewrite envs_lookup_sound => //.
+    rewrite !bi.intuitionistically_if_elim.
+    iDestruct "HΔ" as "(Ha1 & Ha2 & _)".
+    iCombine "Ha1 Ha2" as "Ha".
+    rewrite own_valid is_valid_gives //. }
+  iApply (HΔ with "HΔ") => //.
+Qed.
+
+
+Ltac iCombineOwn_gen_pre Hs_raw lem := 
+  let Hs := words Hs_raw in
+  let get_hyp_type Hname := 
+    let Δ := match goal with | |- environments.envs_entails ?Δ _ => Δ end in
+    let lookup := eval pm_eval in (environments.envs_lookup (INamed Hname) Δ) in
+    match lookup with
+    | Some (_, ?Htype) => constr:(Htype)
+    end
+  in
+  first
+  [ lazymatch Hs with
+    | ?H0n :: ?H1n :: nil => 
+      let H0 := get_hyp_type H0n in (* this may fail if the supplied hypname is not present *)
+      let H1 := get_hyp_type H1n in
+      eapply (lem (INamed H0n) (INamed H1n)); 
+      [ first [reflexivity | fail 2 "Failed to turn"H0"into an own"]
+      | first [reflexivity | fail 2 "Failed to turn"H1"into an own"]
+      | lazymatch goal with
+        | |- proofmode_classes.IsValidOp _ _ ?a1 ?a2 _ =>
+          first [iSolveTC | fail 2 "Did not find a simplification of"a1"â‹…"a2 ]
+        | |- proofmode_classes.IsValidGives _ ?a1 ?a2 _ =>
+          first [iSolveTC | fail 2 "Did not find a consequence of the validity of"a1"â‹…"a2 ]
+        end
+      | reduction.pm_reduce ] (* simplify the envs_delete *)
+    | _ => (fail 1 "Expected exactly two hypothesis, got" Hs_raw)
+    end
+  | fail 1 "One of the supplied hypothesis in"Hs_raw"does not exist" ].
+
+
+Ltac iCombineOwn_op_pre Hs_raw :=
+  iCombineOwn_gen_pre Hs_raw (@tac_own_valid_op).
+
+Ltac iCombineOwn_gives_pre Hs_raw :=
+  iCombineOwn_gen_pre Hs_raw (@tac_own_valid_gives).
+
+
+
+Tactic Notation "iCombineOwn" constr(hyppat) "as" constr(newoppat) "gives" constr(validpat) :=
+  iCombineOwn_op_pre hyppat;
+  iDestruct 1 as newoppat;
+  iDestruct 1 as validpat.
+
+Tactic Notation "iCombineOwn" constr(hyppat) "as" constr(newoppat) "gives" "%" simple_intropattern(validpat) :=
+  iCombineOwn_op_pre hyppat;
+  iDestruct 1 as newoppat;
+  iDestruct 1 as %validpat.
+
+Tactic Notation "iCombineOwn" constr(hyppat) "gives" constr(validpat) :=
+  iCombineOwn_gives_pre hyppat;
+  iDestruct 1 as validpat.
+
+Tactic Notation "iCombineOwn" constr(hyppat) "gives" "%" simple_intropattern(validpat) :=
+  iCombineOwn_gives_pre hyppat;
+  iDestruct 1 as %validpat.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index f2d302e3b8aeb677f7d67abbd5154203db985bfc..f33c0082342a4c4acd22f05dde6dc9c577daf567 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -75,7 +75,7 @@ Qed.
 Lemma ownE_op E1 E2 : E1 ## E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
 Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
 Lemma ownE_disjoint E1 E2 : ownE E1 ∗ ownE E2 ⊢ ⌜E1 ## E2⌝.
-Proof. iIntros "[H1 H2]". iCombineOwn "H1 H2" as "[_ #$]". Qed.
+Proof. iIntros "[H1 H2]". by iCombineOwn "H1 H2" gives %HE. Qed.
 Lemma ownE_op' E1 E2 : ⌜E1 ## E2⌝ ∧ ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
 Proof.
   iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
@@ -93,7 +93,7 @@ Qed.
 Lemma ownD_op E1 E2 : E1 ## E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2.
 Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
 Lemma ownD_disjoint E1 E2 : ownD E1 ∗ ownD E2 ⊢ ⌜E1 ## E2⌝.
-Proof. iIntros "[H1 H2]". iCombineOwn "H1 H2" as "[_ #$]". Qed.
+Proof. iIntros "[H1 H2]". by iCombineOwn "H1 H2" gives %HE. Qed.
 Lemma ownD_op' E1 E2 : ⌜E1 ## E2⌝ ∧ ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2.
 Proof.
   iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
diff --git a/iris/base_logic/proofmode_classes.v b/iris/base_logic/proofmode_classes.v
deleted file mode 100644
index 3b091e78a0bdc0d7e7dd73727b0cb1a2993d8b80..0000000000000000000000000000000000000000
--- a/iris/base_logic/proofmode_classes.v
+++ /dev/null
@@ -1,105 +0,0 @@
-From iris.algebra Require Import cmra.
-From iris.base_logic Require Import own.
-From iris.proofmode Require Import proofmode.
-From iris.prelude Require Import options.
-
-Class IsValidOp {A : cmra} M (a a1 a2 : A) (P : uPred M) := {
-  is_valid_merge : ✓ (a1 ⋅ a2) ⊢ □ P ;
-  is_valid_op : ✓ (a1 ⋅ a2) ⊢@{uPredI M} a ≡ a1 ⋅ a2 ;
-}.
-
-Global Hint Mode IsValidOp ! ! - ! ! - : typeclass_instances.
-
-Definition includedI {M : ucmra} {A : cmra} (a b : A) : uPred M
-  := (∃ c, b ≡ a ⋅ c)%I.
-
-Notation "a ≼ b" := (includedI a b) : bi_scope.
-
-Class IsIncluded {A : cmra} M (a1 a2 : A) (P : uPred M) := 
-  is_included_merge : ✓ a2 ⊢ a1 ≼ a2 ∗-∗ □ P.
-
-Global Hint Mode IsIncluded ! ! ! ! - : typeclass_instances.
-
-(* this is weaker than having a unit! Consider min_natR, agreeR *)
-Class HasRightId {A : cmra} (a : A) :=
-  has_right_id : a ≼ a.
-
-Global Hint Mode HasRightId ! ! : typeclass_instances.
-
-Class IsIncludedOrEq {A : cmra} M (a1 a2 : A) (P_lt P_le : uPred M) := {
-  is_included_or_included : IsIncluded M a1 a2 P_lt;
-  is_included_or_eq_merge : ✓ a2 ⊢ (□ P_lt ∨ a1 ≡ a2) ∗-∗ □ P_le;
-}.
-
-Global Hint Mode IsIncludedOrEq ! ! ! ! - - : typeclass_instances.
-
-
-Section proper.
-  Context {M : ucmra} {A : cmra}.
-  Implicit Types a : A.
-
-  Global Instance includedI_proper_1 : 
-    NonExpansive2 (includedI (M := M) (A := A)).
-  Proof. solve_proper. Qed.
-  Global Instance includedI_proper_2 : 
-    Proper ((≡) ==> (≡) ==> (≡)) (includedI (M := M) (A := A)).
-  Proof. solve_proper. Qed.
-
-  Global Instance is_valid_op_proper :
-    Proper ((≡) ==> (≡) ==> (≡) ==> (=) ==> (iff)) (IsValidOp (A := A) M).
-  Proof.
-    move => a1 a1' Ha1 a2 a2' Ha2 a a' Ha P2' P2 ->.
-    split; case => H1 H2; split.
-    - rewrite -Ha -Ha2 //.
-    - rewrite -Ha -Ha2 -Ha1 //.
-    - rewrite Ha Ha2 //.
-    - rewrite Ha2 Ha Ha1 //.
-  Qed.
-  Lemma is_valid_op_weaken a a1 a2 P1 P2 :
-    IsValidOp M a a1 a2 P1 →
-    (✓ (a1 ⋅ a2) ∗ □ P1 ⊢ P2) →
-    IsValidOp M a a1 a2 P2.
-  Proof.
-    case => HP Ha HP1P2; split; last done.
-    iIntros "#H✓".
-    rewrite -HP1P2.
-    iFrame "#". by rewrite -HP.
-  Qed.
-
-  Global Instance is_included_proper : 
-    Proper ((≡) ==> (≡) ==> (≡) ==> (iff)) (IsIncluded (A := A) M).
-  Proof. solve_proper. Qed.
-  Lemma is_included_weaken a1 a2 P1 P2 :
-    IsIncluded M a1 a2 P1 →
-    (✓ a2 ⊢ □ P1 ∗-∗ □ P2) →
-    IsIncluded M a1 a2 P2.
-  Proof.
-    rewrite /IsIncluded => HP1a HP1P2.
-    iIntros "#H✓". iApply bi.wand_iff_trans.
-    - by iApply HP1a.
-    - by iApply HP1P2.
-  Qed.
-
-  Global Instance is_included_or_eq_proper : 
-    Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (iff)) (IsIncludedOrEq (A := A) M).
-  Proof.
-    move => a1 a1' Ha1 a2 a2' Ha2 P1' P1 HP1 P2' P2 HP2.
-    split; case => H1 H2; split.
-    - revert H1; apply is_included_proper => //.
-    - rewrite -Ha2 -Ha1 -HP1 -HP2 //.
-    - revert H1; apply is_included_proper => //.
-    - rewrite Ha2 Ha1 HP1 HP2 //.
-  Qed.
-  Lemma is_included_or_eq_weaken a1 a2 P1 P2 P3 P4 :
-    IsIncludedOrEq M a1 a2 P1 P2 →
-    (✓ a2 ⊢ □ P1 ∗-∗ □ P3) →
-    (✓ a2 ⊢ □ P2 ∗-∗ □ P4) →
-    IsIncludedOrEq M a1 a2 P3 P4.
-  Proof.
-    case => HP1 HP1P2 HP1P3 HP2P4; split; first by eapply is_included_weaken.
-    iIntros "#H✓". 
-    iApply bi.wand_iff_trans; last by iApply HP2P4.
-    iApply bi.wand_iff_trans; last by iApply HP1P2.
-    iSplit; iIntros "[#HP|$]"; iLeft; by iApply HP1P3.
-  Qed.
-End proper.
\ No newline at end of file
diff --git a/iris/base_logic/validity_tactics.v b/iris/base_logic/validity_tactics.v
deleted file mode 100644
index e55fd87b19f85c642663aa77862b4675dcb5af98..0000000000000000000000000000000000000000
--- a/iris/base_logic/validity_tactics.v
+++ /dev/null
@@ -1,114 +0,0 @@
-From iris.algebra Require Import cmra proofmode_classes auth frac_auth.
-From iris.proofmode Require Import proofmode environments.
-From iris.base_logic Require Import own proofmode_classes proofmode_instances.
-From iris.prelude Require Import options.
-
-(* base lemmas to use the validity typeclasses *)
-
-Lemma own_valid_op {A : cmra} (a a1 a2 : A) γ `{!inG Σ A} (P : iProp Σ) :
-  IsValidOp _ a a1 a2 P →
-  own γ a1 -∗ own γ a2 -∗ own γ a ∗ □ P.
-Proof.
-  case => HP Ha.
-  iIntros "Ha1 Ha2".
-  iAssert (✓ (a1 ⋅ a2))%I as "#H✓".
-  { iApply (own_valid_2 with "Ha1 Ha2"). }
-  iSplit; last by iApply HP.
-  iAssert (a ≡ a1 ⋅ a2)%I with "[Ha1 Ha2]" as "#Heq"; first by iApply Ha.
-  iRewrite "Heq".
-  rewrite own_op; iFrame.
-Qed.
-
-Lemma is_included_auth {A : ucmra} (a1 a2 : A) dq γ `{!inG Σ $ authUR A} (P : iProp Σ) :
-  IsIncluded _ a1 a2 P →
-  own γ (●{dq} a2) -∗ own γ (◯ a1) -∗ □ P.
-Proof.
-  rewrite /IsIncluded => HP.
-  iIntros "Ha1 Ha2".
-  iCombine "Ha1 Ha2" as "Ha".
-  rewrite own_valid auth_both_dfrac_validI.
-  iDestruct "Ha" as "(_ & [%c #Hc] & #H✓)".
-  iApply (HP with "H✓").
-  iExists c. iApply "Hc".
-Qed.
-
-
-(* now their coq tactic variants, for applying them to IPM proofs *)
-
-Lemma tac_own_valid_op {A : cmra} i1 i2 (a a1 a2 : A) p1 p2 γ `{!inG Σ A} (P G : iProp Σ) Δ :
-  envs_lookup i1 Δ = Some (p1, own γ a1) →
-  envs_lookup i2 (envs_delete true i1 p1 Δ) = Some (p2, own γ a2) →
-  IsValidOp _ a a1 a2 P →
-  envs_entails (envs_delete true i2 p2 (envs_delete true i1 p1 Δ)) ((own γ a ∗ □ P) -∗ G)%I →
-  envs_entails Δ G.
-Proof.
-  rewrite envs_entails_eq => Hi1 Hi2 HaP HΔ.
-  erewrite envs_lookup_sound => //.
-  erewrite envs_lookup_sound => //.
-  rewrite !bi.intuitionistically_if_elim HΔ.
-  iIntros "(Ha1 & Ha2 & HaPG)".
-  iApply "HaPG".
-  case: HaP => <- HaP.
-  iDestruct (own_valid_2 with "Ha1 Ha2") as "#H✓".
-  iFrame "#".
-  rewrite HaP.
-  iRewrite "H✓".
-  by iCombine "Ha1 Ha2" as "$".
-Qed.
-
-Lemma tac_auth_included {A : ucmra} i1 i2 (a1 a2 : A) dq p1 p2 γ `{!inG Σ $ authUR A} (P G : iProp Σ) Δ :
-  envs_lookup i1 Δ = Some (p1, own γ (●{dq} a1)) →
-  envs_lookup i2 (envs_delete true i1 p1 Δ) = Some (p2, own γ (◯ a2)) →
-  IsIncluded _ a2 a1 P →
-  envs_entails Δ (□ P -∗ G)%I →
-  envs_entails Δ G.
-Proof.
-  rewrite envs_entails_eq => Hi1 Hi2 HaP HΔ.
-  iIntros "HΔ".
-  iAssert (â–¡ P)%I as "#HP".
-  { erewrite envs_lookup_sound => //.
-    erewrite envs_lookup_sound => //.
-    rewrite !bi.intuitionistically_if_elim.
-    iDestruct "HΔ" as "(Ha1 & Ha2 & _)".
-    iApply (is_included_auth with "Ha1 Ha2") => //. }
-  iApply (HΔ with "HΔ") => //.
-Qed.
-
-
-Ltac iCombineOwn_tac' Hs_raw destructstr := 
-  let Hs := words Hs_raw in
-  let get_hyp_type Hname := 
-    let Δ := match goal with | |- environments.envs_entails ?Δ _ => Δ end in
-    let lookup := eval pm_eval in (environments.envs_lookup (INamed Hname) Δ) in
-    match lookup with
-    | Some (_, ?Htype) => constr:(Htype)
-    end
-  in
-  first
-  [ match Hs with
-    | ?H0n :: ?H1n :: nil =>
-      let H0 := get_hyp_type H0n in
-      let H1 := get_hyp_type H1n in
-      let pr := constr:((H0, H1)) in
-      first 
-      [
-(*      lazymatch pr with
-      | (*(own ?γ (● _), own ?γ (◯ _)) => *) *)
-          eapply (tac_auth_included (INamed H0n) (INamed H1n));
-          [ reflexivity| reflexivity| iSolveTC | ];
-          iIntros destructstr
-      | (*(own ?γ (◯ _), own ?γ (● _)) => *)
-          eapply (tac_auth_included (INamed H1n) (INamed H0n));
-          [ reflexivity| reflexivity| iSolveTC | ];
-          iIntros destructstr
-      | (*_ => *)
-          let tempname := iFresh in
-          iDestruct (own_valid_op with Hs_raw) as tempname;
-          iDestruct tempname as destructstr
-      | fail 4 "Could not find validity lemma for "H0 "and" H1
-      (*end*) ]
-    end
-  | (fail 2 "Expected exactly two hypothesis, got" Hs_raw)].
-
-Tactic Notation "iCombineOwn" constr(hypstr) "as" constr(destructstr) :=
-  iCombineOwn_tac' hypstr destructstr.
\ No newline at end of file
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 7591548c6561c07fb234302691e7fe5dd9bc8163..30f2ebe5af79b8e02d342ca1a8fd86da6b11d0ae 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -78,7 +78,7 @@ Proof.
   iMod (Hwp (OwnPGS _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
     first by rewrite /ownP; iFrame.
   iIntros "!> Hσ". iExists ∅. iMod "H" as (σ2') "[Hσf %]".
-  by iCombineOwn "Hσf Hσ" as "#->".
+  by iCombineOwn "Hσf Hσ" gives %->%leibniz_equiv.
 Qed.
 
 
@@ -93,10 +93,10 @@ Section lifting.
     state_interp σ1 ns κs nt -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
   Proof.
     iIntros "Hσ● Hσ◯". rewrite /ownP.
-    by iCombineOwn "Hσ● Hσ◯" as "#->".
+    by iCombineOwn "Hσ● Hσ◯" gives %?.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
-  Proof. iIntros "[H1 H2]". iCombineOwn "H1 H2" as "[_ []]". Qed.
+  Proof. iIntros "[H1 H2]". iCombineOwn "H1 H2" gives %[]. Qed.
   Global Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ).
   Proof. rewrite /ownP; apply _. Qed.
 
diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index 7a1c3f25fa64dff074d33e8d1e58255e5371f1f6..83f17bd41641b59591cb0f6b261d92ab6e6e0ab7 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -54,7 +54,7 @@ Section mono_proof.
     wp_pures. wp_bind (CmpXchg _ _ _).
     iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
-    - iCombineOwn "Hγ Hγf" as "%Hnc".
+    - iCombineOwn "Hγ Hγf" gives %Hnc.
       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γ".
@@ -75,7 +75,7 @@ Section mono_proof.
     iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
     wp_load.
-    iCombineOwn "Hγ Hγf" as "%Hjc".
+    iCombineOwn "Hγ Hγf" gives %Hjc.
     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|].
@@ -147,7 +147,7 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
-    iCombineOwn "Hγ Hγf" as "[[_ %Hnc] _]".
+    iCombineOwn "Hγ Hγf" gives %[[_ Hnc] _].
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
   Qed.
@@ -158,7 +158,7 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
-    iCombineOwn "Hγ Hγf" as "(_ & _ & <-)".
+    iCombineOwn "Hγ Hγf" gives %(_ & _ & <-%leibniz_equiv).
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists n; by iFrame|].
     by iApply "HΦ".
   Qed.
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index 439734a2067b1b9ddbe981c6f334e8df729d9fca..bfaba53e41aacb2fcd3c1916c717bc92b08caa98 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -71,7 +71,7 @@ Proof.
   - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
     + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
       wp_pures. by iApply "HΦ".
-    + iCombineOwn "Hγ Hγ'" as "[_ []]".
+    + iCombineOwn "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 f2290dd7017778804316f4f033220a105d430729..40348f9eb0798ab05196e588b898421a6c73d34f 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -34,7 +34,7 @@ Section proof.
   Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
 
   Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
-  Proof. iIntros "H1 H2". iCombineOwn "H1 H2" as "[_ []]". Qed.
+  Proof. iIntros "H1 H2". iCombineOwn "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 3270bbd8085283302127c6b5b2e093be2baf8b01..dcc4bd53ca6f79c0650f151c8b589f756ce6902a 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -67,7 +67,7 @@ Section proof.
   Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
   Proof.
     iIntros "[%σ1 H1] [%σ2 H2]".
-    iCombineOwn "H1 H2" as "[_ []]".
+    iCombineOwn "H1 H2" gives %[].
   Qed.
 
   Lemma is_lock_iff γ lk R1 R2 :
@@ -105,7 +105,7 @@ Section proof.
         { iNext. iExists o, n. iFrame. }
         wp_pures. case_bool_decide; [|done]. wp_if.
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
-      + iCombineOwn "Ht Haown" as "[H %Ho]". set_solver.
+      + iCombineOwn "Ht Haown" gives %Ho. set_solver.
     - iModIntro. iSplitL "Hlo Hln Ha".
       { iNext. iExists o, n. by iFrame. }
       wp_pures. case_bool_decide; [simplify_eq |].
@@ -149,15 +149,15 @@ Section proof.
     wp_lam. wp_proj. wp_bind (! _)%E.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
     wp_load.
-    iCombineOwn "Hauth Hγo" as "[-> _]". rename o' into o.
+    iCombineOwn "Hauth Hγo" gives %[<-%leibniz_equiv _].
     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.
-    iCombineOwn "Hauth Hγo" as "[-> _]". rename o' into o.
+    iCombineOwn "Hauth Hγo" gives %[<-%leibniz_equiv _].
     iDestruct "Haown" as "[[Hγo' _]|Haown]".
-    { iCombineOwn "Hγo Hγo'" as "[_ []]". }
+    { iCombineOwn "Hγo Hγo'" gives %[]. }
     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))). }