From 6fbff46e181150523dda49d9bec0ebdccd602d34 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Mar 2017 00:07:19 +0100
Subject: [PATCH] Generic big operators that are no longer tied to CMRAs.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Instead, I have introduced a type class `Monoid` that is used by the big operators:

    Class Monoid {M : ofeT} (o : M → M → M) := {
      monoid_unit : M;
      monoid_ne : NonExpansive2 o;
      monoid_assoc : Assoc (≡) o;
      monoid_comm : Comm (≡) o;
      monoid_left_id : LeftId (≡) monoid_unit o;
      monoid_right_id : RightId (≡) monoid_unit o;
    }.

Note that the operation is an argument because we want to have multiple monoids over
the same type (for example, on `uPred`s we have monoids for `∗`, `∧`, and `∨`). However,
we do bundle the unit because:

- If we would not, the unit would appear explicitly in an implicit argument of the
  big operators, which confuses rewrite. By bundling the unit in the `Monoid` class
  it is hidden, and hence rewrite won't even see it.
- The unit is unique.

We could in principle have big ops over setoids instead of OFEs. However, since we do
not have a canonical structure for bundled setoids, I did not go that way.
---
 _CoqProject                           |   3 +-
 theories/algebra/auth.v               |   3 +-
 theories/algebra/big_op.v             | 493 ++++++++++++++++++++++
 theories/algebra/cmra.v               |  43 +-
 theories/algebra/cmra_big_op.v        | 572 +-------------------------
 theories/algebra/cmra_tactics.v       |  67 ---
 theories/algebra/csum.v               |   5 -
 theories/algebra/gmap.v               |   9 +-
 theories/algebra/list.v               |  60 +++
 theories/algebra/monoid.v             |  47 +++
 theories/base_logic/big_op.v          | 231 +++--------
 theories/base_logic/derived.v         |  59 +++
 theories/base_logic/lib/auth.v        |   5 +-
 theories/base_logic/lib/own.v         |   7 +-
 theories/program_logic/ectx_lifting.v |   5 +-
 theories/program_logic/ownp.v         |   4 +-
 16 files changed, 739 insertions(+), 874 deletions(-)
 create mode 100644 theories/algebra/big_op.v
 delete mode 100644 theories/algebra/cmra_tactics.v
 create mode 100644 theories/algebra/monoid.v

diff --git a/_CoqProject b/_CoqProject
index 784ef81cb..fd5bd12a3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,8 +1,9 @@
 -Q theories iris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+theories/algebra/monoid.v
 theories/algebra/cmra.v
+theories/algebra/big_op.v
 theories/algebra/cmra_big_op.v
-theories/algebra/cmra_tactics.v
 theories/algebra/sts.v
 theories/algebra/auth.v
 theories/algebra/gmap.v
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index c673326ae..536199c43 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -203,7 +203,8 @@ Lemma auth_frag_op a b : â—¯ (a â‹… b) = â—¯ a â‹… â—¯ b.
 Proof. done. Qed.
 Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
 Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
-Global Instance auth_frag_cmra_homomorphism : UCMRAHomomorphism (Auth None).
+
+Global Instance auth_frag_sep_homomorphism : MonoidHomomorphism op op (Auth None).
 Proof. done. Qed.
 
 Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
new file mode 100644
index 000000000..fcb0367ff
--- /dev/null
+++ b/theories/algebra/big_op.v
@@ -0,0 +1,493 @@
+From iris.algebra Require Export monoid.
+From stdpp Require Import functions gmap gmultiset.
+Set Default Proof Using "Type*".
+Local Existing Instances monoid_ne monoid_assoc monoid_comm
+  monoid_left_id monoid_right_id monoid_proper
+  monoid_homomorphism_ne weak_monoid_homomorphism_proper.
+
+(** We define the following big operators with binders build in:
+
+- The operator [ [^o list] k ↦ x ∈ l, P ] folds over a list [l]. The binder [x]
+  refers to each element at index [k].
+- The operator [ [^o map] k ↦ x ∈ m, P ] folds over a map [m]. The binder [x]
+  refers to each element at index [k].
+- The operator [ [^o set] x ∈ X, P ] folds over a set [X]. The binder [x] refers
+  to each element.
+
+Since these big operators are like quantifiers, they have the same precedence as
+[∀] and [∃]. *)
+
+(** * Big ops over lists *)
+Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
+  match xs with
+  | [] => monoid_unit
+  | x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
+  end.
+Instance: Params (@big_opL) 4.
+Arguments big_opL {M} o {_ A} _ !_ /.
+Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
+  (at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
+   format "[^ o  list]  k ↦ x  ∈  l ,  P") : C_scope.
+Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
+  (at level 200, o at level 1, l at level 10, x at level 1, right associativity,
+   format "[^ o  list]  x  ∈  l ,  P") : C_scope.
+
+Definition big_opM `{Monoid M o} `{Countable K} {A} (f : K → A → M)
+    (m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
+Instance: Params (@big_opM) 7.
+Arguments big_opM {M} o {_ K _ _ A} _ _ : simpl never.
+Typeclasses Opaque big_opM.
+Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
+  (at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
+   format "[^  o  map]  k ↦ x  ∈  m ,  P") : C_scope.
+Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
+  (at level 200, o at level 1, m at level 10, x at level 1, right associativity,
+   format "[^ o  map]  x  ∈  m ,  P") : C_scope.
+
+Definition big_opS `{Monoid M o} `{Countable A} (f : A → M)
+  (X : gset A) : M := big_opL o (λ _, f) (elements X).
+Instance: Params (@big_opS) 6.
+Arguments big_opS {M} o {_ A _ _} _ _ : simpl never.
+Typeclasses Opaque big_opS.
+Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
+  (at level 200, o at level 1, X at level 10, x at level 1, right associativity,
+   format "[^ o  set]  x  ∈  X ,  P") : C_scope.
+
+Definition big_opMS `{Monoid M o} `{Countable A} (f : A → M)
+  (X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
+Instance: Params (@big_opMS) 7.
+Arguments big_opMS {M} o {_ A _ _} _ _ : simpl never.
+Typeclasses Opaque big_opMS.
+Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
+  (at level 200, o at level 1, X at level 10, x at level 1, right associativity,
+   format "[^ o  mset]  x  ∈  X ,  P") : C_scope.
+
+(** * Properties about big ops *)
+Section big_op.
+Context `{Monoid M o}.
+Implicit Types xs : list M.
+Infix "`o`" := o (at level 50, left associativity).
+
+(** ** Big ops over lists *)
+Section list.
+  Context {A : Type}.
+  Implicit Types l : list A.
+  Implicit Types f g : nat → A → M.
+
+  Lemma big_opL_nil f : ([^o list] k↦y ∈ [], f k y) = monoid_unit.
+  Proof. done. Qed.
+  Lemma big_opL_cons f x l :
+    ([^o list] k↦y ∈ x :: l, f k y) = f 0 x `o` [^o list] k↦y ∈ l, f (S k) y.
+  Proof. done. Qed.
+  Lemma big_opL_singleton f x : ([^o list] k↦y ∈ [x], f k y) ≡ f 0 x.
+  Proof. by rewrite /= right_id. Qed.
+  Lemma big_opL_app f l1 l2 :
+    ([^o list] k↦y ∈ l1 ++ l2, f k y)
+    ≡ ([^o list] k↦y ∈ l1, f k y) `o` ([^o list] k↦y ∈ l2, f (length l1 + k) y).
+  Proof.
+    revert f. induction l1 as [|x l1 IH]=> f /=; first by rewrite left_id.
+    by rewrite IH assoc.
+  Qed.
+
+  Lemma big_opL_forall R f g l :
+    Reflexive R →
+    Proper (R ==> R ==> R) o →
+    (∀ k y, l !! k = Some y → R (f k y) (g k y)) →
+    R ([^o list] k ↦ y ∈ l, f k y) ([^o list] k ↦ y ∈ l, g k y).
+  Proof.
+    intros ??. revert f g. induction l as [|x l IH]=> f g ? //=; f_equiv; eauto.
+  Qed.
+
+  Lemma big_opL_ext f g l :
+    (∀ k y, l !! k = Some y → f k y = g k y) →
+    ([^o list] k ↦ y ∈ l, f k y) = [^o list] k ↦ y ∈ l, g k y.
+  Proof. apply big_opL_forall; apply _. Qed.
+  Lemma big_opL_proper f g l :
+    (∀ k y, l !! k = Some y → f k y ≡ g k y) →
+    ([^o list] k ↦ y ∈ l, f k y) ≡ ([^o list] k ↦ y ∈ l, g k y).
+  Proof. apply big_opL_forall; apply _. Qed.
+
+  Lemma big_opL_permutation (f : A → M) l1 l2 :
+    l1 ≡ₚ l2 → ([^o list] x ∈ l1, f x) ≡ ([^o list] x ∈ l2, f x).
+  Proof.
+    induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
+    - by rewrite IH.
+    - by rewrite !assoc (comm _ (f x)).
+    - by etrans.
+  Qed.
+  Global Instance big_opL_permutation' (f : A → M) :
+    Proper ((≡ₚ) ==> (≡)) (big_opL o (λ _, f)).
+  Proof. intros xs1 xs2. apply big_opL_permutation. Qed.
+
+  Global Instance big_opL_ne n :
+    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==>
+            eq ==> dist n) (big_opL o (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_opL_proper' :
+    Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> eq ==> (≡))
+           (big_opL o (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
+
+  Lemma big_opL_consZ_l (f : Z → A → M) x l :
+    ([^o list] k↦y ∈ x :: l, f k y) = f 0 x `o` [^o list] k↦y ∈ l, f (1 + k)%Z y.
+  Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
+  Lemma big_opL_consZ_r (f : Z → A → M) x l :
+    ([^o list] k↦y ∈ x :: l, f k y) = f 0 x `o` [^o list] k↦y ∈ l, f (k + 1)%Z y.
+  Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
+
+  Lemma big_opL_fmap {B} (h : A → B) (f : nat → B → M) l :
+    ([^o list] k↦y ∈ h <$> l, f k y) ≡ ([^o list] k↦y ∈ l, f k (h y)).
+  Proof. revert f. induction l as [|x l IH]=> f; csimpl=> //. by rewrite IH. Qed.
+
+  Lemma big_opL_opL f g l :
+    ([^o list] k↦x ∈ l, f k x `o` g k x)
+    ≡ ([^o list] k↦x ∈ l, f k x) `o` ([^o list] k↦x ∈ l, g k x).
+  Proof.
+    revert f g; induction l as [|x l IH]=> f g /=; first by rewrite left_id.
+    by rewrite IH -!assoc (assoc _ (g _ _)) [(g _ _ `o` _)]comm -!assoc.
+  Qed.
+End list.
+
+(** ** Big ops over finite maps *)
+Section gmap.
+  Context `{Countable K} {A : Type}.
+  Implicit Types m : gmap K A.
+  Implicit Types f g : K → A → M.
+
+  Lemma big_opM_forall R f g m :
+    Reflexive R → Proper (R ==> R ==> R) o →
+    (∀ k x, m !! k = Some x → R (f k x) (g k x)) →
+    R ([^o map] k ↦ x ∈ m, f k x) ([^o map] k ↦ x ∈ m, g k x).
+  Proof.
+    intros ?? Hf. apply (big_opL_forall R); auto.
+    intros k [i x] ?%elem_of_list_lookup_2. by apply Hf, elem_of_map_to_list.
+  Qed.
+
+  Lemma big_opM_ext f g m :
+    (∀ k x, m !! k = Some x → f k x = g k x) →
+    ([^o map] k ↦ x ∈ m, f k x) = ([^o map] k ↦ x ∈ m, g k x).
+  Proof. apply big_opM_forall; apply _. Qed.
+  Lemma big_opM_proper f g m :
+    (∀ k x, m !! k = Some x → f k x ≡ g k x) →
+    ([^o map] k ↦ x ∈ m, f k x) ≡ ([^o map] k ↦ x ∈ m, g k x).
+  Proof. apply big_opM_forall; apply _. Qed.
+
+  Global Instance big_opM_ne n :
+    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> eq ==> dist n)
+           (big_opM o (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_opM_proper' :
+    Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> eq ==> (≡))
+           (big_opM o (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
+
+  Lemma big_opM_empty f : ([^o map] k↦x ∈ ∅, f k x) = monoid_unit.
+  Proof. by rewrite /big_opM map_to_list_empty. Qed.
+
+  Lemma big_opM_insert f m i x :
+    m !! i = None →
+    ([^o map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x `o` [^o map] k↦y ∈ m, f k y.
+  Proof. intros ?. by rewrite /big_opM map_to_list_insert. Qed.
+
+  Lemma big_opM_delete f m i x :
+    m !! i = Some x →
+    ([^o map] k↦y ∈ m, f k y) ≡ f i x `o` [^o map] k↦y ∈ delete i m, f k y.
+  Proof.
+    intros. rewrite -big_opM_insert ?lookup_delete //.
+    by rewrite insert_delete insert_id.
+  Qed.
+
+  Lemma big_opM_singleton f i x : ([^o map] k↦y ∈ {[i:=x]}, f k y) ≡ f i x.
+  Proof.
+    rewrite -insert_empty big_opM_insert/=; last auto using lookup_empty.
+    by rewrite big_opM_empty right_id.
+  Qed.
+
+  Lemma big_opM_fmap {B} (h : A → B) (f : K → B → M) m :
+    ([^o map] k↦y ∈ h <$> m, f k y) ≡ ([^o map] k↦y ∈ m, f k (h y)).
+  Proof.
+    rewrite /big_opM map_to_list_fmap big_opL_fmap.
+    by apply big_opL_proper=> ? [??].
+  Qed.
+
+  Lemma big_opM_insert_override (f : K → A → M) m i x x' :
+    m !! i = Some x → f i x ≡ f i x' →
+    ([^o map] k↦y ∈ <[i:=x']> m, f k y) ≡ ([^o map] k↦y ∈ m, f k y).
+  Proof.
+    intros ? Hx. rewrite -insert_delete big_opM_insert ?lookup_delete //.
+    by rewrite -Hx -big_opM_delete.
+  Qed.
+
+  Lemma big_opM_fn_insert {B} (g : K → A → B → M) (f : K → B) m i (x : A) b :
+    m !! i = None →
+    ([^o map] k↦y ∈ <[i:=x]> m, g k y (<[i:=b]> f k))
+    ≡ g i x b `o` [^o map] k↦y ∈ m, g k y (f k).
+  Proof.
+    intros. rewrite big_opM_insert // fn_lookup_insert.
+    f_equiv; apply big_opM_proper; auto=> k y ?.
+    by rewrite fn_lookup_insert_ne; last set_solver.
+  Qed.
+  Lemma big_opM_fn_insert' (f : K → M) m i x P :
+    m !! i = None →
+    ([^o map] k↦y ∈ <[i:=x]> m, <[i:=P]> f k) ≡ (P `o` [^o map] k↦y ∈ m, f k).
+  Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed.
+
+  Lemma big_opM_opM f g m :
+    ([^o map] k↦x ∈ m, f k x `o` g k x)
+    ≡ ([^o map] k↦x ∈ m, f k x) `o` ([^o map] k↦x ∈ m, g k x).
+  Proof. rewrite /big_opM -big_opL_opL. by apply big_opL_proper=> ? [??]. Qed.
+End gmap.
+
+
+(** ** Big ops over finite sets *)
+Section gset.
+  Context `{Countable A}.
+  Implicit Types X : gset A.
+  Implicit Types f : A → M.
+
+  Lemma big_opS_forall R f g X :
+    Reflexive R → Proper (R ==> R ==> R) o →
+    (∀ x, x ∈ X → R (f x) (g x)) →
+    R ([^o set] x ∈ X, f x) ([^o set] x ∈ X, g x).
+  Proof.
+    intros ?? Hf. apply (big_opL_forall R); auto.
+    intros k x ?%elem_of_list_lookup_2. by apply Hf, elem_of_elements.
+  Qed.
+
+  Lemma big_opS_ext f g X :
+    (∀ x, x ∈ X → f x = g x) →
+    ([^o set] x ∈ X, f x) = ([^o set] x ∈ X, g x).
+  Proof. apply big_opS_forall; apply _. Qed.
+  Lemma big_opS_proper f g X :
+    (∀ x, x ∈ X → f x ≡ g x) →
+    ([^o set] x ∈ X, f x) ≡ ([^o set] x ∈ X, g x).
+  Proof. apply big_opS_forall; apply _. Qed.
+
+  Global Instance big_opS_ne n :
+    Proper (pointwise_relation _ (dist n) ==> eq ==> dist n) (big_opS o (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_opS_proper' :
+    Proper (pointwise_relation _ (≡) ==> eq ==> (≡)) (big_opS o (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
+
+  Lemma big_opS_empty f : ([^o set] x ∈ ∅, f x) = monoid_unit.
+  Proof. by rewrite /big_opS elements_empty. Qed.
+
+  Lemma big_opS_insert f X x :
+    x ∉ X → ([^o set] y ∈ {[ x ]} ∪ X, f y) ≡ (f x `o` [^o set] y ∈ X, f y).
+  Proof. intros. by rewrite /big_opS elements_union_singleton. Qed.
+  Lemma big_opS_fn_insert {B} (f : A → B → M) h X x b :
+    x ∉ X →
+    ([^o set] y ∈ {[ x ]} ∪ X, f y (<[x:=b]> h y))
+    ≡ f x b `o` [^o set] y ∈ X, f y (h y).
+  Proof.
+    intros. rewrite big_opS_insert // fn_lookup_insert.
+    f_equiv; apply big_opS_proper; auto=> y ?.
+    by rewrite fn_lookup_insert_ne; last set_solver.
+  Qed.
+  Lemma big_opS_fn_insert' f X x P :
+    x ∉ X → ([^o set] y ∈ {[ x ]} ∪ X, <[x:=P]> f y) ≡ (P `o` [^o set] y ∈ X, f y).
+  Proof. apply (big_opS_fn_insert (λ y, id)). Qed.
+
+  Lemma big_opS_union f X Y :
+    X ⊥ Y →
+    ([^o set] y ∈ X ∪ Y, f y) ≡ ([^o set] y ∈ X, f y) `o` ([^o set] y ∈ Y, f y).
+  Proof.
+    intros. induction X as [|x X ? IH] using collection_ind_L.
+    { by rewrite left_id_L big_opS_empty left_id. }
+    rewrite -assoc_L !big_opS_insert; [|set_solver..].
+    by rewrite -assoc IH; last set_solver.
+  Qed.
+
+  Lemma big_opS_delete f X x :
+    x ∈ X → ([^o set] y ∈ X, f y) ≡ f x `o` [^o set] y ∈ X ∖ {[ x ]}, f y.
+  Proof.
+    intros. rewrite -big_opS_insert; last set_solver.
+    by rewrite -union_difference_L; last set_solver.
+  Qed.
+
+  Lemma big_opS_singleton f x : ([^o set] y ∈ {[ x ]}, f y) ≡ f x.
+  Proof. intros. by rewrite /big_opS elements_singleton /= right_id. Qed.
+
+  Lemma big_opS_opS f g X :
+    ([^o set] y ∈ X, f y `o` g y) ≡ ([^o set] y ∈ X, f y) `o` ([^o set] y ∈ X, g y).
+  Proof. by rewrite /big_opS -big_opL_opL. Qed.
+End gset.
+
+Lemma big_opM_dom `{Countable K} {A} (f : K → M) (m : gmap K A) :
+  ([^o map] k↦_ ∈ m, f k) ≡ ([^o set] k ∈ dom _ m, f k).
+Proof.
+  induction m as [|i x ?? IH] using map_ind; [by rewrite dom_empty_L|].
+  by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom.
+Qed.
+
+(** ** Big ops over finite msets *)
+Section gmultiset.
+  Context `{Countable A}.
+  Implicit Types X : gmultiset A.
+  Implicit Types f : A → M.
+
+  Lemma big_opMS_forall R f g X :
+    Reflexive R → Proper (R ==> R ==> R) o →
+    (∀ x, x ∈ X → R (f x) (g x)) →
+    R ([^o mset] x ∈ X, f x) ([^o mset] x ∈ X, g x).
+  Proof.
+    intros ?? Hf. apply (big_opL_forall R); auto.
+    intros k x ?%elem_of_list_lookup_2. by apply Hf, gmultiset_elem_of_elements.
+  Qed.
+
+  Lemma big_opMS_ext f g X :
+    (∀ x, x ∈ X → f x = g x) →
+    ([^o mset] x ∈ X, f x) = ([^o mset] x ∈ X, g x).
+  Proof. apply big_opMS_forall; apply _. Qed.
+  Lemma big_opMS_proper f g X :
+    (∀ x, x ∈ X → f x ≡ g x) →
+    ([^o mset] x ∈ X, f x) ≡ ([^o mset] x ∈ X, g x).
+  Proof. apply big_opMS_forall; apply _. Qed.
+
+  Global Instance big_opMS_ne n :
+    Proper (pointwise_relation _ (dist n) ==> eq ==> dist n) (big_opMS o (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_opMS_proper' :
+    Proper (pointwise_relation _ (≡) ==> eq ==> (≡)) (big_opMS o (A:=A)).
+  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
+
+  Lemma big_opMS_empty f : ([^o mset] x ∈ ∅, f x) = monoid_unit.
+  Proof. by rewrite /big_opMS gmultiset_elements_empty. Qed.
+
+  Lemma big_opMS_union f X Y :
+    ([^o mset] y ∈ X ∪ Y, f y) ≡ ([^o mset] y ∈ X, f y) `o` [^o mset] y ∈ Y, f y.
+  Proof. by rewrite /big_opMS gmultiset_elements_union big_opL_app. Qed.
+
+  Lemma big_opMS_singleton f x : ([^o mset] y ∈ {[ x ]}, f y) ≡ f x.
+  Proof.
+    intros. by rewrite /big_opMS gmultiset_elements_singleton /= right_id.
+  Qed.
+
+  Lemma big_opMS_delete f X x :
+    x ∈ X → ([^o mset] y ∈ X, f y) ≡ f x `o` [^o mset] y ∈ X ∖ {[ x ]}, f y.
+  Proof.
+    intros. rewrite -big_opMS_singleton -big_opMS_union.
+    by rewrite -gmultiset_union_difference'.
+  Qed.
+
+  Lemma big_opMS_opMS f g X :
+    ([^o mset] y ∈ X, f y `o` g y) ≡ ([^o mset] y ∈ X, f y) `o` ([^o mset] y ∈ X, g y).
+  Proof. by rewrite /big_opMS -big_opL_opL. Qed.
+End gmultiset.
+End big_op.
+
+Section homomorphisms.
+  Context `{Monoid M1 o1, Monoid M2 o2}.
+  Infix "`o1`" := o1 (at level 50, left associativity).
+  Infix "`o2`" := o2 (at level 50, left associativity).
+
+  Lemma big_opL_commute {A} (h : M1 → M2) `{!MonoidHomomorphism o1 o2 h}
+      (f : nat → A → M1) l :
+    h ([^o1 list] k↦x ∈ l, f k x) ≡ ([^o2 list] k↦x ∈ l, h (f k x)).
+  Proof.
+    revert f. induction l as [|x l IH]=> f /=.
+    - by rewrite monoid_homomorphism_unit.
+    - by rewrite monoid_homomorphism -IH.
+  Qed.
+  Lemma big_opL_commute1 {A} (h : M1 → M2) `{!WeakMonoidHomomorphism o1 o2 h}
+      (f : nat → A → M1) l :
+    l ≠ [] → h ([^o1 list] k↦x ∈ l, f k x) ≡ ([^o2 list] k↦x ∈ l, h (f k x)).
+  Proof.
+    intros ?. revert f. induction l as [|x [|x' l'] IH]=> f //.
+    - by rewrite !big_opL_singleton.
+    - by rewrite !(big_opL_cons _ x) monoid_homomorphism -IH.
+  Qed.
+
+  Lemma big_opM_commute `{Countable K} {A} (h : M1 → M2)
+      `{!MonoidHomomorphism o1 o2 h} (f : K → A → M1) m :
+    h ([^o1 map] k↦x ∈ m, f k x) ≡ ([^o2 map] k↦x ∈ m, h (f k x)).
+  Proof.
+    intros. induction m as [|i x m ? IH] using map_ind.
+    - by rewrite !big_opM_empty monoid_homomorphism_unit.
+    - by rewrite !big_opM_insert // monoid_homomorphism -IH.
+  Qed.
+  Lemma big_opM_commute1 `{Countable K} {A} (h : M1 → M2)
+      `{!WeakMonoidHomomorphism o1 o2 h} (f : K → A → M1) m :
+    m ≠ ∅ → h ([^o1 map] k↦x ∈ m, f k x) ≡ ([^o2 map] k↦x ∈ m, h (f k x)).
+  Proof.
+    intros. induction m as [|i x m ? IH] using map_ind; [done|].
+    destruct (decide (m = ∅)) as [->|].
+    - by rewrite !big_opM_insert // !big_opM_empty !right_id.
+    - by rewrite !big_opM_insert // monoid_homomorphism -IH //.
+  Qed.
+
+  Lemma big_opS_commute `{Countable A} (h : M1 → M2)
+      `{!MonoidHomomorphism o1 o2 h} (f : A → M1) X :
+    h ([^o1 set] x ∈ X, f x) ≡ ([^o2 set] x ∈ X, h (f x)).
+  Proof.
+    intros. induction X as [|x X ? IH] using collection_ind_L.
+    - by rewrite !big_opS_empty monoid_homomorphism_unit.
+    - by rewrite !big_opS_insert // monoid_homomorphism -IH.
+  Qed.
+  Lemma big_opS_commute1 `{Countable A} (h : M1 → M2)
+      `{!WeakMonoidHomomorphism o1 o2 h} (f : A → M1) X :
+    X ≠ ∅ → h ([^o1 set] x ∈ X, f x) ≡ ([^o2 set] x ∈ X, h (f x)).
+  Proof.
+    intros. induction X as [|x X ? IH] using collection_ind_L; [done|].
+    destruct (decide (X = ∅)) as [->|].
+    - by rewrite !big_opS_insert // !big_opS_empty !right_id.
+    - by rewrite !big_opS_insert // monoid_homomorphism -IH //.
+  Qed.
+
+  Lemma big_opMS_commute `{Countable A} (h : M1 → M2)
+      `{!MonoidHomomorphism o1 o2 h} (f : A → M1) X :
+    h ([^o1 mset] x ∈ X, f x) ≡ ([^o2 mset] x ∈ X, h (f x)).
+  Proof.
+    intros. induction X as [|x X IH] using gmultiset_ind.
+    - by rewrite !big_opMS_empty monoid_homomorphism_unit.
+    - by rewrite !big_opMS_union !big_opMS_singleton monoid_homomorphism -IH.
+  Qed.
+  Lemma big_opMS_commute1 `{Countable A} (h : M1 → M2)
+      `{!WeakMonoidHomomorphism o1 o2 h} (f : A → M1) X :
+    X ≠ ∅ → h ([^o1 mset] x ∈ X, f x) ≡ ([^o2 mset] x ∈ X, h (f x)).
+  Proof.
+    intros. induction X as [|x X IH] using gmultiset_ind; [done|].
+    destruct (decide (X = ∅)) as [->|].
+    - by rewrite !big_opMS_union !big_opMS_singleton !big_opMS_empty !right_id.
+    - by rewrite !big_opMS_union !big_opMS_singleton monoid_homomorphism -IH //.
+  Qed.
+
+  Context `{!LeibnizEquiv M2}.
+
+  Lemma big_opL_commute_L {A} (h : M1 → M2)
+      `{!MonoidHomomorphism o1 o2 h} (f : nat → A → M1) l :
+    h ([^o1 list] k↦x ∈ l, f k x) = ([^o2 list] k↦x ∈ l, h (f k x)).
+  Proof. unfold_leibniz. by apply big_opL_commute. Qed.
+  Lemma big_opL_commute1_L {A} (h : M1 → M2)
+      `{!WeakMonoidHomomorphism o1 o2 h} (f : nat → A → M1) l :
+    l ≠ [] → h ([^o1 list] k↦x ∈ l, f k x) = ([^o2 list] k↦x ∈ l, h (f k x)).
+  Proof. unfold_leibniz. by apply big_opL_commute1. Qed.
+
+  Lemma big_opM_commute_L `{Countable K} {A} (h : M1 → M2)
+      `{!MonoidHomomorphism o1 o2 h} (f : K → A → M1) m :
+    h ([^o1 map] k↦x ∈ m, f k x) = ([^o2 map] k↦x ∈ m, h (f k x)).
+  Proof. unfold_leibniz. by apply big_opM_commute. Qed.
+  Lemma big_opM_commute1_L `{Countable K} {A} (h : M1 → M2)
+      `{!WeakMonoidHomomorphism o1 o2 h} (f : K → A → M1) m :
+    m ≠ ∅ → h ([^o1 map] k↦x ∈ m, f k x) = ([^o2 map] k↦x ∈ m, h (f k x)).
+  Proof. unfold_leibniz. by apply big_opM_commute1. Qed.
+
+  Lemma big_opS_commute_L `{Countable A} (h : M1 → M2)
+      `{!MonoidHomomorphism o1 o2 h} (f : A → M1) X :
+    h ([^o1 set] x ∈ X, f x) = ([^o2 set] x ∈ X, h (f x)).
+  Proof. unfold_leibniz. by apply big_opS_commute. Qed.
+  Lemma big_opS_commute1_L `{ Countable A} (h : M1 → M2)
+      `{!WeakMonoidHomomorphism o1 o2 h} (f : A → M1) X :
+    X ≠ ∅ → h ([^o1 set] x ∈ X, f x) = ([^o2 set] x ∈ X, h (f x)).
+  Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opS_commute1. Qed.
+
+  Lemma big_opMS_commute_L `{Countable A} (h : M1 → M2)
+      `{!MonoidHomomorphism o1 o2 h} (f : A → M1) X :
+    h ([^o1 mset] x ∈ X, f x) = ([^o2 mset] x ∈ X, h (f x)).
+  Proof. unfold_leibniz. by apply big_opMS_commute. Qed.
+  Lemma big_opMS_commute1_L `{Countable A} (h : M1 → M2)
+      `{!WeakMonoidHomomorphism o1 o2 h} (f : A → M1) X :
+    X ≠ ∅ → h ([^o1 mset] x ∈ X, f x) = ([^o2 mset] x ∈ X, h (f x)).
+  Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opMS_commute1. Qed.
+End homomorphisms.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index eac3265ee..d1556b415 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export ofe.
+From iris.algebra Require Export ofe monoid.
 Set Default Proof Using "Type".
 
 Class PCore (A : Type) := pcore : A → option A.
@@ -243,20 +243,6 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
 Arguments cmra_monotone_validN {_ _} _ {_} _ _ _.
 Arguments cmra_monotone {_ _} _ {_} _ _ _.
 
-(* Not all intended homomorphisms preserve validity, in particular it does not
-hold for the [ownM] and [own] connectives. *)
-Class CMRAHomomorphism {A B : cmraT} (f : A → B) := {
-  cmra_homomorphism_ne :> NonExpansive f;
-  cmra_homomorphism x y : f (x ⋅ y) ≡ f x ⋅ f y
-}.
-Arguments cmra_homomorphism {_ _} _ _ _ _.
-
-Class UCMRAHomomorphism {A B : ucmraT} (f : A → B) := {
-  ucmra_homomorphism :> CMRAHomomorphism f;
-  ucmra_homomorphism_unit : f ∅ ≡ ∅
-}.
-Arguments ucmra_homomorphism_unit {_ _} _ _.
-
 (** * Properties **)
 Section cmra.
 Context {A : cmraT}.
@@ -633,9 +619,12 @@ Section ucmra.
   Qed.
   Global Instance empty_cancelable : Cancelable (∅:A).
   Proof. intros ???. by rewrite !left_id. Qed.
+
+  (* For big ops *)
+  Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := ∅ |}.
 End ucmra.
-Hint Immediate cmra_unit_total.
 
+Hint Immediate cmra_unit_total.
 
 (** * Properties about CMRAs with Leibniz equality *)
 Section cmra_leibniz.
@@ -752,26 +741,6 @@ Section cmra_monotone.
   Proof. rewrite !cmra_valid_validN; eauto using cmra_monotone_validN. Qed.
 End cmra_monotone.
 
-Instance cmra_homomorphism_id {A : cmraT} : CMRAHomomorphism (@id A).
-Proof. repeat split; by try apply _. Qed.
-Instance cmra_homomorphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
-  CMRAHomomorphism f → CMRAHomomorphism g → CMRAHomomorphism (g ∘ f).
-Proof.
-  split.
-  - apply _.
-  - move=> x y /=. rewrite -(cmra_homomorphism g).
-    by apply (ne_proper _), cmra_homomorphism.
-Qed.
-
-Instance cmra_homomorphism_proper {A B : cmraT} (f : A → B) :
-  CMRAHomomorphism f → Proper ((≡) ==> (≡)) f := λ _, ne_proper _.
-
-Instance ucmra_homomorphism_id {A : ucmraT} : UCMRAHomomorphism (@id A).
-Proof. repeat split; by try apply _. Qed.
-Instance ucmra_homomorphism_compose {A B C : ucmraT} (f : A → B) (g : B → C) :
-  UCMRAHomomorphism f → UCMRAHomomorphism g → UCMRAHomomorphism (g ∘ f).
-Proof. split. apply _. by rewrite /= !ucmra_homomorphism_unit. Qed.
-
 (** Functors *)
 Structure rFunctor := RFunctor {
   rFunctor_car : ofeT → ofeT → cmraT;
@@ -1316,8 +1285,6 @@ Section option.
   (** Misc *)
   Global Instance Some_cmra_monotone : CMRAMonotone Some.
   Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed.
-  Global Instance Some_cmra_homomorphism : CMRAHomomorphism Some.
-  Proof. split. apply _. done. Qed.
 
   Lemma op_None mx my : mx ⋅ my = None ↔ mx = None ∧ my = None.
   Proof. destruct mx, my; naive_solver. Qed.
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index 9fba43e70..54122de3e 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -1,465 +1,17 @@
-From iris.algebra Require Export cmra list.
-From stdpp Require Import functions gmap gmultiset.
-Set Default Proof Using "Type".
-
-(** The operator [ [â‹…] Ps ] folds [â‹…] over the list [Ps]. This operator is not a
-quantifier, so it binds strongly.
-
-Apart from that, we define the following big operators with binders build in:
-
-- The operator [ [⋅ list] k ↦ x ∈ l, P ] folds over a list [l]. The binder [x]
-  refers to each element at index [k].
-- The operator [ [⋅ map] k ↦ x ∈ m, P ] folds over a map [m]. The binder [x]
-  refers to each element at index [k].
-- The operator [ [⋅ set] x ∈ X, P ] folds over a set [X]. The binder [x] refers
-  to each element.
-
-Since these big operators are like quantifiers, they have the same precedence as
-[∀] and [∃]. *)
-
-(** * Big ops over lists *)
-Fixpoint big_opL {M : ucmraT} {A} (f : nat → A → M) (xs : list A) : M :=
-  match xs with
-  | [] => ∅
-  | x :: xs => f 0 x ⋅ big_opL (λ n, f (S n)) xs
-  end.
-Instance: Params (@big_opL) 2.
-Arguments big_opL _ _ _ !_ /.
-Notation "'[⋅' 'list' ] k ↦ x ∈ l , P" := (big_opL (λ k x, P) l)
-  (at level 200, l at level 10, k, x at level 1, right associativity,
-   format "[⋅  list ]  k ↦ x  ∈  l ,  P") : C_scope.
-Notation "'[⋅' 'list' ] x ∈ l , P" := (big_opL (λ _ x, P) l)
-  (at level 200, l at level 10, x at level 1, right associativity,
-   format "[⋅  list ]  x  ∈  l ,  P") : C_scope.
-
-Notation "'[⋅]' xs" := (big_opL (λ _ x, x) xs) (at level 20) : C_scope.
-
-Definition big_opM {M : ucmraT} `{Countable K} {A} (f : K → A → M)
-    (m : gmap K A) : M := big_opL (λ _, curry f) (map_to_list m).
-Instance: Params (@big_opM) 6.
-Typeclasses Opaque big_opM.
-Notation "'[⋅' 'map' ] k ↦ x ∈ m , P" := (big_opM (λ k x, P) m)
-  (at level 200, m at level 10, k, x at level 1, right associativity,
-   format "[⋅  map ]  k ↦ x  ∈  m ,  P") : C_scope.
-Notation "'[⋅' 'map' ] x ∈ m , P" := (big_opM (λ _ x, P) m)
-  (at level 200, m at level 10, x at level 1, right associativity,
-   format "[⋅  map ]  x  ∈  m ,  P") : C_scope.
-
-Definition big_opS {M : ucmraT} `{Countable A} (f : A → M)
-  (X : gset A) : M := big_opL (λ _, f) (elements X).
-Instance: Params (@big_opS) 5.
-Typeclasses Opaque big_opS.
-Notation "'[⋅' 'set' ] x ∈ X , P" := (big_opS (λ x, P) X)
-  (at level 200, X at level 10, x at level 1, right associativity,
-   format "[⋅  set ]  x  ∈  X ,  P") : C_scope.
-
-Definition big_opMS {M : ucmraT} `{Countable A} (f : A → M)
-  (X : gmultiset A) : M := big_opL (λ _, f) (elements X).
-Instance: Params (@big_opMS) 5.
-Typeclasses Opaque big_opMS.
-Notation "'[⋅' 'mset' ] x ∈ X , P" := (big_opMS (λ x, P) X)
-  (at level 200, X at level 10, x at level 1, right associativity,
-   format "[⋅  'mset' ]  x  ∈  X ,  P") : C_scope.
-
-(** * Properties about big ops *)
-Section big_op.
-Context {M : ucmraT}.
-Implicit Types xs : list M.
-
-(** ** Big ops over lists *)
-Section list.
-  Context {A : Type}.
-  Implicit Types l : list A.
-  Implicit Types f g : nat → A → M.
-
-  Lemma big_opL_nil f : ([⋅ list] k↦y ∈ nil, f k y) = ∅.
-  Proof. done. Qed.
-  Lemma big_opL_cons f x l :
-    ([⋅ list] k↦y ∈ x :: l, f k y) = f 0 x ⋅ [⋅ list] k↦y ∈ l, f (S k) y.
-  Proof. done. Qed.
-  Lemma big_opL_singleton f x : ([⋅ list] k↦y ∈ [x], f k y) ≡ f 0 x.
-  Proof. by rewrite /= right_id. Qed.
-  Lemma big_opL_app f l1 l2 :
-    ([⋅ list] k↦y ∈ l1 ++ l2, f k y)
-    ≡ ([⋅ list] k↦y ∈ l1, f k y) ⋅ ([⋅ list] k↦y ∈ l2, f (length l1 + k) y).
-  Proof.
-    revert f. induction l1 as [|x l1 IH]=> f /=; first by rewrite left_id.
-    by rewrite IH assoc.
-  Qed.
-
-  Lemma big_opL_forall R f g l :
-    Reflexive R →
-    Proper (R ==> R ==> R) (@op M _) →
-    (∀ k y, l !! k = Some y → R (f k y) (g k y)) →
-    R ([⋅ list] k ↦ y ∈ l, f k y) ([⋅ list] k ↦ y ∈ l, g k y).
-  Proof.
-    intros ??. revert f g. induction l as [|x l IH]=> f g ? //=; f_equiv; eauto.
-  Qed.
-
-  Lemma big_opL_mono f g l :
-    (∀ k y, l !! k = Some y → f k y ≼ g k y) →
-    ([⋅ list] k ↦ y ∈ l, f k y) ≼ [⋅ list] k ↦ y ∈ l, g k y.
-  Proof. apply big_opL_forall; apply _. Qed.
-  Lemma big_opL_ext f g l :
-    (∀ k y, l !! k = Some y → f k y = g k y) →
-    ([⋅ list] k ↦ y ∈ l, f k y) = [⋅ list] k ↦ y ∈ l, g k y.
-  Proof. apply big_opL_forall; apply _. Qed.
-  Lemma big_opL_proper f g l :
-    (∀ k y, l !! k = Some y → f k y ≡ g k y) →
-    ([⋅ list] k ↦ y ∈ l, f k y) ≡ ([⋅ list] k ↦ y ∈ l, g k y).
-  Proof. apply big_opL_forall; apply _. Qed.
-
-  Lemma big_opL_permutation (f : A → M) l1 l2 :
-    l1 ≡ₚ l2 → ([⋅ list] x ∈ l1, f x) ≡ ([⋅ list] x ∈ l2, f x).
-  Proof.
-    induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
-    - by rewrite IH.
-    - by rewrite !assoc (comm _ (f x)).
-    - by etrans.
-  Qed.
-  Global Instance big_op_permutation (f : A → M) :
-    Proper ((≡ₚ) ==> (≡)) (big_opL (λ _, f)).
-  Proof. intros xs1 xs2. apply big_opL_permutation. Qed.
-
-  Lemma big_opL_submseteq (f : A → M) l1 l2 :
-    l1 ⊆+ l2 → ([⋅ list] x ∈ l1, f x) ≼ ([⋅ list] x ∈ l2, f x).
-  Proof.
-    intros [xs' ->]%submseteq_Permutation.
-    rewrite big_opL_app; apply cmra_included_l.
-  Qed.
-
-  Global Instance big_opL_ne n :
-    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==>
-            eq ==> dist n) (big_opL (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opL_proper' :
-    Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> eq ==> (≡))
-           (big_opL (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opL_mono' :
-    Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> eq ==> (≼))
-           (big_opL (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
-
-  Lemma big_opL_consZ_l (f : Z → A → M) x l :
-    ([⋅ list] k↦y ∈ x :: l, f k y) = f 0 x ⋅ [⋅ list] k↦y ∈ l, f (1 + k)%Z y.
-  Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
-  Lemma big_opL_consZ_r (f : Z → A → M) x l :
-    ([⋅ list] k↦y ∈ x :: l, f k y) = f 0 x ⋅ [⋅ list] k↦y ∈ l, f (k + 1)%Z y.
-  Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
-
-  Lemma big_opL_lookup f l i x :
-    l !! i = Some x → f i x ≼ [⋅ list] k↦y ∈ l, f k y.
-  Proof.
-    intros. rewrite -(take_drop_middle l i x) // big_opL_app big_opL_cons.
-    rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl.
-    eapply transitivity, cmra_included_r; eauto using cmra_included_l.
-  Qed.
-
-  Lemma big_opL_elem_of (f : A → M) l x : x ∈ l → f x ≼ [⋅ list] y ∈ l, f y.
-  Proof.
-    intros [i ?]%elem_of_list_lookup; eauto using (big_opL_lookup (λ _, f)).
-  Qed.
-
-  Lemma big_opL_fmap {B} (h : A → B) (f : nat → B → M) l :
-    ([⋅ list] k↦y ∈ h <$> l, f k y) ≡ ([⋅ list] k↦y ∈ l, f k (h y)).
-  Proof. revert f. induction l as [|x l IH]=> f; csimpl=> //. by rewrite IH. Qed.
-
-  Lemma big_opL_opL f g l :
-    ([⋅ list] k↦x ∈ l, f k x ⋅ g k x)
-    ≡ ([⋅ list] k↦x ∈ l, f k x) ⋅ ([⋅ list] k↦x ∈ l, g k x).
-  Proof.
-    revert f g; induction l as [|x l IH]=> f g /=; first by rewrite left_id.
-    by rewrite IH -!assoc (assoc _ (g _ _)) [(g _ _ â‹… _)]comm -!assoc.
-  Qed.
-End list.
-
-(** ** Big ops over finite maps *)
-Section gmap.
-  Context `{Countable K} {A : Type}.
-  Implicit Types m : gmap K A.
-  Implicit Types f g : K → A → M.
-
-  Lemma big_opM_forall R f g m :
-    Reflexive R → Proper (R ==> R ==> R) (@op M _) →
-    (∀ k x, m !! k = Some x → R (f k x) (g k x)) →
-    R ([⋅ map] k ↦ x ∈ m, f k x) ([⋅ map] k ↦ x ∈ m, g k x).
-  Proof.
-    intros ?? Hf. apply (big_opL_forall R); auto.
-    intros k [i x] ?%elem_of_list_lookup_2. by apply Hf, elem_of_map_to_list.
-  Qed.
-
-  Lemma big_opM_mono f g m1 m2 :
-    m1 ⊆ m2 → (∀ k x, m2 !! k = Some x → f k x ≼ g k x) →
-    ([⋅ map] k ↦ x ∈ m1, f k x) ≼ [⋅ map] k ↦ x ∈ m2, g k x.
-  Proof.
-    intros Hm Hf. trans ([⋅ map] k↦x ∈ m2, f k x).
-    - by apply big_opL_submseteq, map_to_list_submseteq.
-    - apply big_opM_forall; apply _ || auto.
-  Qed.
-  Lemma big_opM_ext f g m :
-    (∀ k x, m !! k = Some x → f k x = g k x) →
-    ([⋅ map] k ↦ x ∈ m, f k x) = ([⋅ map] k ↦ x ∈ m, g k x).
-  Proof. apply big_opM_forall; apply _. Qed.
-  Lemma big_opM_proper f g m :
-    (∀ k x, m !! k = Some x → f k x ≡ g k x) →
-    ([⋅ map] k ↦ x ∈ m, f k x) ≡ ([⋅ map] k ↦ x ∈ m, g k x).
-  Proof. apply big_opM_forall; apply _. Qed.
-
-  Global Instance big_opM_ne n :
-    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> eq ==> dist n)
-           (big_opM (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opM_proper' :
-    Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> eq ==> (≡))
-           (big_opM (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opM_mono' :
-    Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> eq ==> (≼))
-           (big_opM (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
-
-  Lemma big_opM_empty f : ([⋅ map] k↦x ∈ ∅, f k x) = ∅.
-  Proof. by rewrite /big_opM map_to_list_empty. Qed.
-
-  Lemma big_opM_insert f m i x :
-    m !! i = None →
-    ([⋅ map] k↦y ∈ <[i:=x]> m, f k y) ≡ f i x ⋅ [⋅ map] k↦y ∈ m, f k y.
-  Proof. intros ?. by rewrite /big_opM map_to_list_insert. Qed.
-
-  Lemma big_opM_delete f m i x :
-    m !! i = Some x →
-    ([⋅ map] k↦y ∈ m, f k y) ≡ f i x ⋅ [⋅ map] k↦y ∈ delete i m, f k y.
-  Proof.
-    intros. rewrite -big_opM_insert ?lookup_delete //.
-    by rewrite insert_delete insert_id.
-  Qed.
-
-  Lemma big_opM_lookup f m i x :
-    m !! i = Some x → f i x ≼ [⋅ map] k↦y ∈ m, f k y.
-  Proof. intros. rewrite big_opM_delete //. apply cmra_included_l. Qed.
-  Lemma big_opM_lookup_dom (f : K → M) m i :
-    is_Some (m !! i) → f i ≼ [⋅ map] k↦_ ∈ m, f k.
-  Proof. intros [x ?]. by eapply (big_opM_lookup (λ i x, f i)). Qed.
-
-  Lemma big_opM_singleton f i x : ([⋅ map] k↦y ∈ {[i:=x]}, f k y) ≡ f i x.
-  Proof.
-    rewrite -insert_empty big_opM_insert/=; last auto using lookup_empty.
-    by rewrite big_opM_empty right_id.
-  Qed.
-
-  Lemma big_opM_fmap {B} (h : A → B) (f : K → B → M) m :
-    ([⋅ map] k↦y ∈ h <$> m, f k y) ≡ ([⋅ map] k↦y ∈ m, f k (h y)).
-  Proof.
-    rewrite /big_opM map_to_list_fmap big_opL_fmap.
-    by apply big_opL_proper=> ? [??].
-  Qed.
-
-  Lemma big_opM_insert_override (f : K → A → M) m i x x' :
-    m !! i = Some x → f i x ≡ f i x' →
-    ([⋅ map] k↦y ∈ <[i:=x']> m, f k y) ≡ ([⋅ map] k↦y ∈ m, f k y).
-  Proof.
-    intros ? Hx. rewrite -insert_delete big_opM_insert ?lookup_delete //.
-    by rewrite -Hx -big_opM_delete.
-  Qed.
-
-  Lemma big_opM_fn_insert {B} (g : K → A → B → M) (f : K → B) m i (x : A) b :
-    m !! i = None →
-      ([⋅ map] k↦y ∈ <[i:=x]> m, g k y (<[i:=b]> f k))
-    ≡ (g i x b ⋅ [⋅ map] k↦y ∈ m, g k y (f k)).
-  Proof.
-    intros. rewrite big_opM_insert // fn_lookup_insert.
-    apply cmra_op_proper', big_opM_proper; auto=> k y ?.
-    by rewrite fn_lookup_insert_ne; last set_solver.
-  Qed.
-  Lemma big_opM_fn_insert' (f : K → M) m i x P :
-    m !! i = None →
-    ([⋅ map] k↦y ∈ <[i:=x]> m, <[i:=P]> f k) ≡ (P ⋅ [⋅ map] k↦y ∈ m, f k).
-  Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed.
-
-  Lemma big_opM_opM f g m :
-    ([⋅ map] k↦x ∈ m, f k x ⋅ g k x)
-    ≡ ([⋅ map] k↦x ∈ m, f k x) ⋅ ([⋅ map] k↦x ∈ m, g k x).
-  Proof. rewrite /big_opM -big_opL_opL. by apply big_opL_proper=> ? [??]. Qed.
-End gmap.
-
-
-(** ** Big ops over finite sets *)
-Section gset.
-  Context `{Countable A}.
-  Implicit Types X : gset A.
-  Implicit Types f : A → M.
-
-  Lemma big_opS_forall R f g X :
-    Reflexive R → Proper (R ==> R ==> R) (@op M _) →
-    (∀ x, x ∈ X → R (f x) (g x)) →
-    R ([⋅ set] x ∈ X, f x) ([⋅ set] x ∈ X, g x).
-  Proof.
-    intros ?? Hf. apply (big_opL_forall R); auto.
-    intros k x ?%elem_of_list_lookup_2. by apply Hf, elem_of_elements.
-  Qed.
-
-  Lemma big_opS_mono f g X Y :
-    X ⊆ Y → (∀ x, x ∈ Y → f x ≼ g x) →
-    ([⋅ set] x ∈ X, f x) ≼ [⋅ set] x ∈ Y, g x.
-  Proof.
-    intros HX Hf. trans ([⋅ set] x ∈ Y, f x).
-    - by apply big_opL_submseteq, elements_submseteq.
-    - apply big_opS_forall; apply _ || auto.
-  Qed.
-  Lemma big_opS_ext f g X :
-    (∀ x, x ∈ X → f x = g x) →
-    ([⋅ set] x ∈ X, f x) = ([⋅ set] x ∈ X, g x).
-  Proof. apply big_opS_forall; apply _. Qed.
-  Lemma big_opS_proper f g X :
-    (∀ x, x ∈ X → f x ≡ g x) →
-    ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, g x).
-  Proof. apply big_opS_forall; apply _. Qed.
-
-  Global Instance big_opS_ne n :
-    Proper (pointwise_relation _ (dist n) ==> eq ==> dist n) (big_opS (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opS_proper' :
-    Proper (pointwise_relation _ (≡) ==> eq ==> (≡)) (big_opS (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opS_mono' :
-    Proper (pointwise_relation _ (≼) ==> eq ==> (≼)) (big_opS (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
-
-  Lemma big_opS_empty f : ([⋅ set] x ∈ ∅, f x) = ∅.
-  Proof. by rewrite /big_opS elements_empty. Qed.
-
-  Lemma big_opS_insert f X x :
-    x ∉ X → ([⋅ set] y ∈ {[ x ]} ∪ X, f y) ≡ (f x ⋅ [⋅ set] y ∈ X, f y).
-  Proof. intros. by rewrite /big_opS elements_union_singleton. Qed.
-  Lemma big_opS_fn_insert {B} (f : A → B → M) h X x b :
-    x ∉ X →
-       ([⋅ set] y ∈ {[ x ]} ∪ X, f y (<[x:=b]> h y))
-    ≡ (f x b ⋅ [⋅ set] y ∈ X, f y (h y)).
-  Proof.
-    intros. rewrite big_opS_insert // fn_lookup_insert.
-    apply cmra_op_proper', big_opS_proper; auto=> y ?.
-    by rewrite fn_lookup_insert_ne; last set_solver.
-  Qed.
-  Lemma big_opS_fn_insert' f X x P :
-    x ∉ X → ([⋅ set] y ∈ {[ x ]} ∪ X, <[x:=P]> f y) ≡ (P ⋅ [⋅ set] y ∈ X, f y).
-  Proof. apply (big_opS_fn_insert (λ y, id)). Qed.
-
-  Lemma big_opS_union f X Y :
-    X ⊥ Y →
-    ([⋅ set] y ∈ X ∪ Y, f y) ≡ ([⋅ set] y ∈ X, f y) ⋅ ([⋅ set] y ∈ Y, f y).
-  Proof.
-    intros. induction X as [|x X ? IH] using collection_ind_L.
-    { by rewrite left_id_L big_opS_empty left_id. }
-    rewrite -assoc_L !big_opS_insert; [|set_solver..].
-    by rewrite -assoc IH; last set_solver.
-  Qed.
-
-  Lemma big_opS_delete f X x :
-    x ∈ X → ([⋅ set] y ∈ X, f y) ≡ f x ⋅ [⋅ set] y ∈ X ∖ {[ x ]}, f y.
-  Proof.
-    intros. rewrite -big_opS_insert; last set_solver.
-    by rewrite -union_difference_L; last set_solver.
-  Qed.
-
-  Lemma big_opS_elem_of f X x : x ∈ X → f x ≼ [⋅ set] y ∈ X, f y.
-  Proof. intros. rewrite big_opS_delete //. apply cmra_included_l. Qed.
-
-  Lemma big_opS_singleton f x : ([⋅ set] y ∈ {[ x ]}, f y) ≡ f x.
-  Proof. intros. by rewrite /big_opS elements_singleton /= right_id. Qed.
-
-  Lemma big_opS_opS f g X :
-    ([⋅ set] y ∈ X, f y ⋅ g y) ≡ ([⋅ set] y ∈ X, f y) ⋅ ([⋅ set] y ∈ X, g y).
-  Proof. by rewrite /big_opS -big_opL_opL. Qed.
-End gset.
-
-Lemma big_opM_dom `{Countable K} {A} (f : K → M) (m : gmap K A) :
-  ([⋅ map] k↦_ ∈ m, f k) ≡ ([⋅ set] k ∈ dom _ m, f k).
-Proof.
-  induction m as [|i x ?? IH] using map_ind; [by rewrite dom_empty_L|].
-  by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom.
-Qed.
-
-(** ** Big ops over finite msets *)
-Section gmultiset.
-  Context `{Countable A}.
-  Implicit Types X : gmultiset A.
-  Implicit Types f : A → M.
-
-  Lemma big_opMS_forall R f g X :
-    Reflexive R → Proper (R ==> R ==> R) (@op M _) →
-    (∀ x, x ∈ X → R (f x) (g x)) →
-    R ([⋅ mset] x ∈ X, f x) ([⋅ mset] x ∈ X, g x).
-  Proof.
-    intros ?? Hf. apply (big_opL_forall R); auto.
-    intros k x ?%elem_of_list_lookup_2. by apply Hf, gmultiset_elem_of_elements.
-  Qed.
-
-  Lemma big_opMS_mono f g X Y :
-    X ⊆ Y → (∀ x, x ∈ Y → f x ≼ g x) →
-    ([⋅ mset] x ∈ X, f x) ≼ [⋅ mset] x ∈ Y, g x.
-  Proof.
-    intros HX Hf. trans ([⋅ mset] x ∈ Y, f x).
-    - by apply big_opL_submseteq, gmultiset_elements_submseteq.
-    - apply big_opMS_forall; apply _ || auto.
-  Qed.
-  Lemma big_opMS_ext f g X :
-    (∀ x, x ∈ X → f x = g x) →
-    ([⋅ mset] x ∈ X, f x) = ([⋅ mset] x ∈ X, g x).
-  Proof. apply big_opMS_forall; apply _. Qed.
-  Lemma big_opMS_proper f g X :
-    (∀ x, x ∈ X → f x ≡ g x) →
-    ([⋅ mset] x ∈ X, f x) ≡ ([⋅ mset] x ∈ X, g x).
-  Proof. apply big_opMS_forall; apply _. Qed.
-
-  Global Instance big_opMS_ne n :
-    Proper (pointwise_relation _ (dist n) ==> eq ==> dist n) (big_opMS (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opMS_proper' :
-    Proper (pointwise_relation _ (≡) ==> eq ==> (≡)) (big_opMS (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opMS_mono' :
-    Proper (pointwise_relation _ (≼) ==> eq ==> (≼)) (big_opMS (M:=M) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
-
-  Lemma big_opMS_empty f : ([⋅ mset] x ∈ ∅, f x) = ∅.
-  Proof. by rewrite /big_opMS gmultiset_elements_empty. Qed.
-
-  Lemma big_opMS_union f X Y :
-    ([⋅ mset] y ∈ X ∪ Y, f y) ≡ ([⋅ mset] y ∈ X, f y) ⋅ [⋅ mset] y ∈ Y, f y.
-  Proof. by rewrite /big_opMS gmultiset_elements_union big_opL_app. Qed.
-
-  Lemma big_opMS_singleton f x : ([⋅ mset] y ∈ {[ x ]}, f y) ≡ f x.
-  Proof.
-    intros. by rewrite /big_opMS gmultiset_elements_singleton /= right_id.
-  Qed.
-
-  Lemma big_opMS_delete f X x :
-    x ∈ X → ([⋅ mset] y ∈ X, f y) ≡ f x ⋅ [⋅ mset] y ∈ X ∖ {[ x ]}, f y.
-  Proof.
-    intros. rewrite -big_opMS_singleton -big_opMS_union.
-    by rewrite -gmultiset_union_difference'.
-  Qed.
-
-  Lemma big_opMS_elem_of f X x : x ∈ X → f x ≼ [⋅ mset] y ∈ X, f y.
-  Proof. intros. rewrite big_opMS_delete //. apply cmra_included_l. Qed.
-
-  Lemma big_opMS_opMS f g X :
-    ([⋅ mset] y ∈ X, f y ⋅ g y) ≡ ([⋅ mset] y ∈ X, f y) ⋅ ([⋅ mset] y ∈ X, g y).
-  Proof. by rewrite /big_opMS -big_opL_opL. Qed.
-End gmultiset.
-End big_op.
+From iris.algebra Require Export big_op cmra.
+From stdpp Require Import gmap gmultiset.
+Set Default Proof Using "Type*".
 
 (** Option *)
 Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l :
-  ([⋅ list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None.
+  ([^op list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None.
 Proof.
   revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
   - intros [??] [|k] y ?; naive_solver.
   - intros Hl. split. by apply (Hl 0). intros k. apply (Hl (S k)).
 Qed.
 Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K → A → option M) m :
-  ([⋅ map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
+  ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
 Proof.
   induction m as [|i x m ? IH] using map_ind=> //=.
   rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split.
@@ -469,124 +21,16 @@ Proof.
   - intros k y ?. apply (Hm k). by simplify_map_eq.
 Qed.
 Lemma big_opS_None {M : cmraT} `{Countable A} (f : A → option M) X :
-  ([⋅ set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
+  ([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
   induction X as [|x X ? IH] using collection_ind_L; [done|].
   rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver.
 Qed.
 Lemma big_opMS_None {M : cmraT} `{Countable A} (f : A → option M) X :
-  ([⋅ mset] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
+  ([^op mset] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
   induction X as [|x X IH] using gmultiset_ind.
   { rewrite big_opMS_empty. set_solver. }
   rewrite -equiv_None big_opMS_union big_opMS_singleton equiv_None op_None IH.
   set_solver.
-Qed.
-
-(** Commuting with respect to homomorphisms *)
-Lemma big_opL_commute {M1 M2 : ucmraT} {A} (h : M1 → M2)
-    `{!UCMRAHomomorphism h} (f : nat → A → M1) l :
-  h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)).
-Proof.
-  revert f. induction l as [|x l IH]=> f /=.
-  - by rewrite ucmra_homomorphism_unit.
-  - by rewrite cmra_homomorphism -IH.
-Qed.
-Lemma big_opL_commute1 {M1 M2 : ucmraT} {A} (h : M1 → M2)
-    `{!CMRAHomomorphism h} (f : nat → A → M1) l :
-  l ≠ [] → h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)).
-Proof.
-  intros ?. revert f. induction l as [|x [|x' l'] IH]=> f //.
-  - by rewrite !big_opL_singleton.
-  - by rewrite !(big_opL_cons _ x) cmra_homomorphism -IH.
-Qed.
-
-Lemma big_opM_commute {M1 M2 : ucmraT} `{Countable K} {A} (h : M1 → M2)
-    `{!UCMRAHomomorphism h} (f : K → A → M1) m :
-  h ([⋅ map] k↦x ∈ m, f k x) ≡ ([⋅ map] k↦x ∈ m, h (f k x)).
-Proof.
-  intros. induction m as [|i x m ? IH] using map_ind.
-  - by rewrite !big_opM_empty ucmra_homomorphism_unit.
-  - by rewrite !big_opM_insert // cmra_homomorphism -IH.
-Qed.
-Lemma big_opM_commute1 {M1 M2 : ucmraT} `{Countable K} {A} (h : M1 → M2)
-    `{!CMRAHomomorphism h} (f : K → A → M1) m :
-  m ≠ ∅ → h ([⋅ map] k↦x ∈ m, f k x) ≡ ([⋅ map] k↦x ∈ m, h (f k x)).
-Proof.
-  intros. induction m as [|i x m ? IH] using map_ind; [done|].
-  destruct (decide (m = ∅)) as [->|].
-  - by rewrite !big_opM_insert // !big_opM_empty !right_id.
-  - by rewrite !big_opM_insert // cmra_homomorphism -IH //.
-Qed.
-
-Lemma big_opS_commute {M1 M2 : ucmraT} `{Countable A}
-    (h : M1 → M2) `{!UCMRAHomomorphism h} (f : A → M1) X :
-  h ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, h (f x)).
-Proof.
-  intros. induction X as [|x X ? IH] using collection_ind_L.
-  - by rewrite !big_opS_empty ucmra_homomorphism_unit.
-  - by rewrite !big_opS_insert // cmra_homomorphism -IH.
-Qed.
-Lemma big_opS_commute1 {M1 M2 : ucmraT} `{Countable A}
-    (h : M1 → M2) `{!CMRAHomomorphism h} (f : A → M1) X :
-  X ≠ ∅ → h ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, h (f x)).
-Proof.
-  intros. induction X as [|x X ? IH] using collection_ind_L; [done|].
-  destruct (decide (X = ∅)) as [->|].
-  - by rewrite !big_opS_insert // !big_opS_empty !right_id.
-  - by rewrite !big_opS_insert // cmra_homomorphism -IH //.
-Qed.
-
-Lemma big_opMS_commute {M1 M2 : ucmraT} `{Countable A}
-    (h : M1 → M2) `{!UCMRAHomomorphism h} (f : A → M1) X :
-  h ([⋅ mset] x ∈ X, f x) ≡ ([⋅ mset] x ∈ X, h (f x)).
-Proof.
-  intros. induction X as [|x X IH] using gmultiset_ind.
-  - by rewrite !big_opMS_empty ucmra_homomorphism_unit.
-  - by rewrite !big_opMS_union !big_opMS_singleton cmra_homomorphism -IH.
-Qed.
-Lemma big_opMS_commute1 {M1 M2 : ucmraT} `{Countable A}
-    (h : M1 → M2) `{!CMRAHomomorphism h} (f : A → M1) X :
-  X ≠ ∅ → h ([⋅ mset] x ∈ X, f x) ≡ ([⋅ mset] x ∈ X, h (f x)).
-Proof.
-  intros. induction X as [|x X IH] using gmultiset_ind; [done|].
-  destruct (decide (X = ∅)) as [->|].
-  - by rewrite !big_opMS_union !big_opMS_singleton !big_opMS_empty !right_id.
-  - by rewrite !big_opMS_union !big_opMS_singleton cmra_homomorphism -IH //.
-Qed.
-
-Lemma big_opL_commute_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2} {A}
-    (h : M1 → M2) `{!UCMRAHomomorphism h} (f : nat → A → M1) l :
-  h ([⋅ list] k↦x ∈ l, f k x) = ([⋅ list] k↦x ∈ l, h (f k x)).
-Proof. unfold_leibniz. by apply big_opL_commute. Qed.
-Lemma big_opL_commute1_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2} {A}
-    (h : M1 → M2) `{!CMRAHomomorphism h} (f : nat → A → M1) l :
-  l ≠ [] → h ([⋅ list] k↦x ∈ l, f k x) = ([⋅ list] k↦x ∈ l, h (f k x)).
-Proof. unfold_leibniz. by apply big_opL_commute1. Qed.
-
-Lemma big_opM_commute_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable K} {A}
-    (h : M1 → M2) `{!UCMRAHomomorphism h} (f : K → A → M1) m :
-  h ([⋅ map] k↦x ∈ m, f k x) = ([⋅ map] k↦x ∈ m, h (f k x)).
-Proof. unfold_leibniz. by apply big_opM_commute. Qed.
-Lemma big_opM_commute1_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable K} {A}
-    (h : M1 → M2) `{!CMRAHomomorphism h} (f : K → A → M1) m :
-  m ≠ ∅ → h ([⋅ map] k↦x ∈ m, f k x) = ([⋅ map] k↦x ∈ m, h (f k x)).
-Proof. unfold_leibniz. by apply big_opM_commute1. Qed.
-
-Lemma big_opS_commute_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable A}
-    (h : M1 → M2) `{!UCMRAHomomorphism h} (f : A → M1) X :
-  h ([⋅ set] x ∈ X, f x) = ([⋅ set] x ∈ X, h (f x)).
-Proof. unfold_leibniz. by apply big_opS_commute. Qed.
-Lemma big_opS_commute1_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable A}
-    (h : M1 → M2) `{!CMRAHomomorphism h} (f : A → M1) X :
-  X ≠ ∅ → h ([⋅ set] x ∈ X, f x) = ([⋅ set] x ∈ X, h (f x)).
-Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opS_commute1. Qed.
-
-Lemma big_opMS_commute_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable A}
-    (h : M1 → M2) `{!UCMRAHomomorphism h} (f : A → M1) X :
-  h ([⋅ mset] x ∈ X, f x) = ([⋅ mset] x ∈ X, h (f x)).
-Proof. unfold_leibniz. by apply big_opMS_commute. Qed.
-Lemma big_opMS_commute1_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable A}
-    (h : M1 → M2) `{!CMRAHomomorphism h} (f : A → M1) X :
-  X ≠ ∅ → h ([⋅ mset] x ∈ X, f x) = ([⋅ mset] x ∈ X, h (f x)).
-Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opMS_commute1. Qed.
+Qed.
\ No newline at end of file
diff --git a/theories/algebra/cmra_tactics.v b/theories/algebra/cmra_tactics.v
deleted file mode 100644
index b94b625ad..000000000
--- a/theories/algebra/cmra_tactics.v
+++ /dev/null
@@ -1,67 +0,0 @@
-From iris.algebra Require Export cmra.
-From iris.algebra Require Import cmra_big_op.
-Set Default Proof Using "Type".
-
-(** * Simple solver for validity and inclusion by reflection *)
-Module ra_reflection. Section ra_reflection.
-  Context  {A : ucmraT}.
-
-  Inductive expr :=
-    | EVar : nat → expr
-    | EEmpty : expr
-    | EOp : expr → expr → expr.
-  Fixpoint eval (Σ : list A) (e : expr) : A :=
-    match e with
-    | EVar n => from_option id ∅ (Σ !! n)
-    | EEmpty => ∅
-    | EOp e1 e2 => eval Σ e1 ⋅ eval Σ e2
-    end.
-  Fixpoint flatten (e : expr) : list nat :=
-    match e with
-    | EVar n => [n]
-    | EEmpty => []
-    | EOp e1 e2 => flatten e1 ++ flatten e2
-    end.
-  Lemma eval_flatten Σ e :
-    eval Σ e ≡ [⋅ list] n ∈ flatten e, from_option id ∅ (Σ !! n).
-  Proof.
-    induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //.
-    by rewrite IH1 IH2 big_opL_app.
-  Qed.
-  Lemma flatten_correct Σ e1 e2 :
-    flatten e1 ⊆+ flatten e2 → eval Σ e1 ≼ eval Σ e2.
-  Proof.
-    by intros He; rewrite !eval_flatten; apply big_opL_submseteq; rewrite ->He.
-  Qed.
-
-  Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
-  Global Instance quote_empty: Quote E1 E1 ∅ EEmpty.
-  Global Instance quote_var Σ1 Σ2 e i:
-    rlist.QuoteLookup Σ1 Σ2 e i → Quote Σ1 Σ2 e (EVar i) | 1000.
-  Global Instance quote_app Σ1 Σ2 Σ3 x1 x2 e1 e2 :
-    Quote Σ1 Σ2 x1 e1 → Quote Σ2 Σ3 x2 e2 → Quote Σ1 Σ3 (x1 ⋅ x2) (EOp e1 e2).
-  End ra_reflection.
-
-  Ltac quote :=
-    match goal with
-    | |- @included _ _ _ ?x ?y =>
-      lazymatch type of (_ : Quote [] _ x _) with Quote _ ?Σ2 _ ?e1 =>
-      lazymatch type of (_ : Quote Σ2 _ y _) with Quote _ ?Σ3 _ ?e2 =>
-        change (eval Σ3 e1 ≼ eval Σ3 e2)
-      end end
-    end.
-End ra_reflection.
-
-Ltac solve_included :=
-  ra_reflection.quote;
-  apply ra_reflection.flatten_correct, (bool_decide_unpack _);
-  vm_compute; apply I.
-
-Ltac solve_validN :=
-  match goal with
-  | H : ✓{?n} ?y |- ✓{?n'} ?x =>
-     let Hn := fresh in let Hx := fresh in
-     assert (n' ≤ n) as Hn by omega;
-     assert (x ≼ y) as Hx by solve_included;
-     eapply cmra_validN_le, Hn; eapply cmra_validN_included, Hx; apply H
-  end.
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index fedeab9db..1a786c352 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -281,11 +281,6 @@ Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
 Global Instance Cinr_id_free b : IdFree b → IdFree (Cinr b).
 Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
 
-Global Instance Cinl_cmra_homomorphism : CMRAHomomorphism Cinl.
-Proof. split. apply _. done. Qed.
-Global Instance Cinr_cmra_homomorphism : CMRAHomomorphism Cinr.
-Proof. split. apply _. done. Qed.
-
 (** Internalized properties *)
 Lemma csum_equivI {M} (x y : csum A B) :
   x ≡ y ⊣⊢ (match x, y with
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 52b9e0ccc..77556eebd 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -200,9 +200,9 @@ Implicit Types m : gmap K A.
 Implicit Types i : K.
 Implicit Types x y : A.
 
-Global Instance lookup_cmra_homomorphism :
-  UCMRAHomomorphism (lookup i : gmap K A → option A).
-Proof. split. split. apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
+Global Instance lookup_op_homomorphism :
+  MonoidHomomorphism op op (lookup i : gmap K A → option A).
+Proof. split; [split|]. apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
 
 Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i)).
 Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
@@ -247,9 +247,6 @@ Qed.
 Lemma op_singleton (i : K) (x y : A) :
   {[ i := x ]} â‹… {[ i := y ]} = ({[ i := x â‹… y ]} : gmap K A).
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
-Global Instance singleton_cmra_homomorphism :
-  CMRAHomomorphism (singletonM i : A → gmap K A).
-Proof. split. apply _. intros. by rewrite op_singleton. Qed.
 
 Global Instance gmap_persistent m : (∀ x : A, Persistent x) → Persistent m.
 Proof.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 3b378c3db..21d183d78 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -464,3 +464,63 @@ Instance listURF_contractive F :
 Proof.
   by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, urFunctor_contractive.
 Qed.
+
+(** * Persistence and timelessness of lists of uPreds *)
+Class PersistentL {M} (Ps : list (uPred M)) :=
+  persistentL : Forall PersistentP Ps.
+Arguments persistentL {_} _ {_}.
+Hint Mode PersistentL + ! : typeclass_instances.
+
+Class TimelessL {M} (Ps : list (uPred M)) :=
+  timelessL : Forall TimelessP Ps.
+Arguments timelessL {_} _ {_}.
+Hint Mode TimelessP + ! : typeclass_instances.
+
+Section persistent_timeless.
+  Context {M : ucmraT}.
+  Implicit Types Ps Qs : list (uPred M).
+  Implicit Types A : Type.
+
+  Global Instance nil_persistentL : PersistentL (@nil (uPred M)).
+  Proof. constructor. Qed.
+  Global Instance cons_persistentL P Ps :
+    PersistentP P → PersistentL Ps → PersistentL (P :: Ps).
+  Proof. by constructor. Qed.
+  Global Instance app_persistentL Ps Ps' :
+    PersistentL Ps → PersistentL Ps' → PersistentL (Ps ++ Ps').
+  Proof. apply Forall_app_2. Qed.
+
+  Global Instance fmap_persistentL {A} (f : A → uPred M) xs :
+    (∀ x, PersistentP (f x)) → PersistentL (f <$> xs).
+  Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
+  Global Instance zip_with_persistentL {A B} (f : A → B → uPred M) xs ys :
+    (∀ x y, PersistentP (f x y)) → PersistentL (zip_with f xs ys).
+  Proof.
+    unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
+  Qed.
+  Global Instance imap_persistentL {A} (f : nat → A → uPred M) xs :
+    (∀ i x, PersistentP (f i x)) → PersistentL (imap f xs).
+  Proof. revert f. induction xs; simpl; constructor; naive_solver. Qed.
+
+  (** ** Timelessness *)
+  Global Instance nil_timelessL : TimelessL (@nil (uPred M)).
+  Proof. constructor. Qed.
+  Global Instance cons_timelessL P Ps :
+    TimelessP P → TimelessL Ps → TimelessL (P :: Ps).
+  Proof. by constructor. Qed.
+  Global Instance app_timelessL Ps Ps' :
+    TimelessL Ps → TimelessL Ps' → TimelessL (Ps ++ Ps').
+  Proof. apply Forall_app_2. Qed.
+
+  Global Instance fmap_timelessL {A} (f : A → uPred M) xs :
+    (∀ x, TimelessP (f x)) → TimelessL (f <$> xs).
+  Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
+  Global Instance zip_with_timelessL {A B} (f : A → B → uPred M) xs ys :
+    (∀ x y, TimelessP (f x y)) → TimelessL (zip_with f xs ys).
+  Proof.
+    unfold TimelessL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
+  Qed.
+  Global Instance imap_timelessL {A} (f : nat → A → uPred M) xs :
+    (∀ i x, TimelessP (f i x)) → TimelessL (imap f xs).
+  Proof. revert f. induction xs; simpl; constructor; naive_solver. Qed.
+End persistent_timeless.
diff --git a/theories/algebra/monoid.v b/theories/algebra/monoid.v
new file mode 100644
index 000000000..f933e57d0
--- /dev/null
+++ b/theories/algebra/monoid.v
@@ -0,0 +1,47 @@
+From iris.algebra Require Export ofe.
+Set Default Proof Using "Type".
+
+(** The Monoid class that is used for generic big operators in the file
+[algebra/big_op]. The operation is an argument because we want to have multiple
+monoids over the same type (for example, on [uPred]s we have monoids for [∗],
+[∧], and [∨]). However, we do bundle the unit because:
+
+- If we would not, it would appear explicitly in an argument of the big
+  operators, which confuses rewrite. Now it is hidden in the class, and hence
+  rewrite won't even see it.
+- The unit is unique.
+
+We could in principle have big ops over setoids instead of OFEs. However, since
+we do not have a canonical structure for setoids, we do not go that way.
+
+Note that we do not declare any of the projections as type class instances. That
+is because we only need them in the [big_op] file, and nowhere else. Hence, we
+declare these instances locally there to avoid them being used elsewhere. *)
+Class Monoid {M : ofeT} (o : M → M → M) := {
+  monoid_unit : M;
+  monoid_ne : NonExpansive2 o;
+  monoid_assoc : Assoc (≡) o;
+  monoid_comm : Comm (≡) o;
+  monoid_left_id : LeftId (≡) monoid_unit o;
+  monoid_right_id : RightId (≡) monoid_unit o;
+}.
+Lemma monoid_proper `{Monoid M o} : Proper ((≡) ==> (≡) ==> (≡)) o.
+Proof. apply ne_proper_2, monoid_ne. Qed.
+
+(** The [Homomorphism] classes give rise to generic lemmas about big operators
+commuting with each other. *)
+Class WeakMonoidHomomorphism {M1 M2 : ofeT} (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2)
+    `{Monoid M1 o1, Monoid M2 o2} (f : M1 → M2) := {
+  monoid_homomorphism_ne : NonExpansive f;
+  monoid_homomorphism x y : f (o1 x y) ≡ o2 (f x) (f y)
+}.
+
+Class MonoidHomomorphism {M1 M2 : ofeT} (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2)
+    `{Monoid M1 o1, Monoid M2 o2} (f : M1 → M2) := {
+  monoid_homomorphism_weak :> WeakMonoidHomomorphism o1 o2 f;
+  monoid_homomorphism_unit : f monoid_unit ≡ monoid_unit
+}.
+
+Lemma weak_monoid_homomorphism_proper
+  `{WeakMonoidHomomorphism M1 M2 o1 o2 f} : Proper ((≡) ==> (≡)) f.
+Proof. apply ne_proper, monoid_homomorphism_ne. Qed.
diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 9b494709e..43b745d9d 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -1,125 +1,34 @@
-From iris.algebra Require Export list cmra_big_op.
+From iris.algebra Require Export list big_op.
 From iris.base_logic Require Export base_logic.
 From stdpp Require Import gmap fin_collections gmultiset functions.
 Set Default Proof Using "Type".
 Import uPred.
 
-(* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc)
-CMRA structure on uPred. *)
-Section cmra.
-  Context {M : ucmraT}.
-
-  Instance uPred_valid_inst : Valid (uPred M) := λ P, ∀ n x, ✓{n} x → P n x.
-  Instance uPred_validN_inst : ValidN (uPred M) := λ n P,
-    ∀ n' x, n' ≤ n → ✓{n'} x → P n' x.
-  Instance uPred_op : Op (uPred M) := uPred_sep.
-  Instance uPred_pcore : PCore (uPred M) := λ _, Some True%I.
-
-  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN_inst n).
-  Proof. intros P Q HPQ; split=> H n' x ??; by apply HPQ, H. Qed.
-
-  Lemma uPred_validN_alt n (P : uPred M) : ✓{n} P → P ≡{n}≡ True%I.
-  Proof.
-    unseal=> HP; split=> n' x ??; split; [done|].
-    intros _. by apply HP.
-  Qed.
-
-  Lemma uPred_cmra_validN_op_l n P Q : ✓{n} (P ∗ Q)%I → ✓{n} P.
-  Proof.
-    unseal. intros HPQ n' x ??.
-    destruct (HPQ n' x) as (x1&x2&->&?&?); auto.
-    eapply uPred_mono with x1; eauto using cmra_includedN_l.
-  Qed.
-
-  Lemma uPred_included P Q : P ≼ Q → Q ⊢ P.
-  Proof. intros [P' ->]. apply sep_elim_l. Qed.
-
-  Definition uPred_cmra_mixin : CMRAMixin (uPred M).
-  Proof.
-    apply cmra_total_mixin; try apply _ || by eauto.
-    - intros n P Q ??. by ofe_subst.
-    - intros P; split.
-      + intros HP n n' x ?. apply HP.
-      + intros HP n x. by apply (HP n).
-    - intros n P HP n' x ?. apply HP; auto.
-    - intros P. by rewrite left_id.
-    - intros P Q _. exists True%I. by rewrite left_id.
-    - intros n P Q. apply uPred_cmra_validN_op_l.
-    - intros n P Q1 Q2 HP HPQ. exists True%I, P; split_and!.
-      + by rewrite left_id.
-      + move: HP; by rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt.
-      + move: HP; rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt=> ->.
-        by rewrite left_id.
-  Qed.
-
-  Canonical Structure uPredR := CMRAT (uPred M) uPred_cmra_mixin.
-
-  Instance uPred_empty : Empty (uPred M) := True%I.
-
-  Definition uPred_ucmra_mixin : UCMRAMixin (uPred M).
-  Proof.
-    split; last done.
-    - by rewrite /empty /uPred_empty uPred_pure_eq.
-    - intros P. by rewrite left_id.
-  Qed.
-
-  Canonical Structure uPredUR := UCMRAT (uPred M) uPred_ucmra_mixin.
-
-  Global Instance uPred_always_homomorphism : UCMRAHomomorphism uPred_always.
-  Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
-  Global Instance uPred_always_if_homomorphism b :
-    UCMRAHomomorphism (uPred_always_if b).
-  Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
-  Global Instance uPred_later_homomorphism : UCMRAHomomorphism uPred_later.
-  Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
-  Global Instance uPred_laterN_homomorphism n : UCMRAHomomorphism (uPred_laterN n).
-  Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed.
-  Global Instance uPred_except_0_homomorphism :
-    CMRAHomomorphism uPred_except_0.
-  Proof. split. apply _. apply except_0_sep. Qed.
-  Global Instance uPred_ownM_homomorphism : UCMRAHomomorphism uPred_ownM.
-  Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed.
-End cmra.
-
-Arguments uPredR : clear implicits.
-Arguments uPredUR : clear implicits.
-
 (* Notations *)
-Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) (λ k x, P) l)
+Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL uPred_sep (λ k x, P) l)
   (at level 200, l at level 10, k, x at level 1, right associativity,
-   format "[∗  list ]  k ↦ x  ∈  l ,  P") : uPred_scope.
-Notation "'[∗' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) (λ _ x, P) l)
+   format "[∗  list]  k ↦ x  ∈  l ,  P") : uPred_scope.
+Notation "'[∗' 'list]' x ∈ l , P" := (big_opL uPred_sep (λ _ x, P) l)
   (at level 200, l at level 10, x at level 1, right associativity,
-   format "[∗  list ]  x  ∈  l ,  P") : uPred_scope.
+   format "[∗  list]  x  ∈  l ,  P") : uPred_scope.
 
 Notation "'[∗]' Ps" :=
-  (big_opL (M:=uPredUR _) (λ _ x, x) Ps) (at level 20) : uPred_scope.
+  (big_opL uPred_sep (λ _ x, x) Ps) (at level 20) : uPred_scope.
 
-Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) (λ k x, P) m)
+Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM uPred_sep (λ k x, P) m)
   (at level 200, m at level 10, k, x at level 1, right associativity,
-   format "[∗  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
-Notation "'[∗' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) (λ _ x, P) m)
+   format "[∗  map]  k ↦ x  ∈  m ,  P") : uPred_scope.
+Notation "'[∗' 'map]' x ∈ m , P" := (big_opM uPred_sep (λ _ x, P) m)
   (at level 200, m at level 10, x at level 1, right associativity,
-   format "[∗  map ]  x  ∈  m ,  P") : uPred_scope.
+   format "[∗  map]  x  ∈  m ,  P") : uPred_scope.
 
-Notation "'[∗' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) (λ x, P) X)
+Notation "'[∗' 'set]' x ∈ X , P" := (big_opS uPred_sep (λ x, P) X)
   (at level 200, X at level 10, x at level 1, right associativity,
-   format "[∗  set ]  x  ∈  X ,  P") : uPred_scope.
+   format "[∗  set]  x  ∈  X ,  P") : uPred_scope.
 
-Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) (λ x, P) X)
+Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS uPred_sep (λ x, P) X)
   (at level 200, X at level 10, x at level 1, right associativity,
-   format "[∗  mset ]  x  ∈  X ,  P") : uPred_scope.
-
-(** * Persistence and timelessness of lists of uPreds *)
-Class PersistentL {M} (Ps : list (uPred M)) :=
-  persistentL : Forall PersistentP Ps.
-Arguments persistentL {_} _ {_}.
-Hint Mode PersistentL + ! : typeclass_instances.
-
-Class TimelessL {M} (Ps : list (uPred M)) :=
-  timelessL : Forall TimelessP Ps.
-Arguments timelessL {_} _ {_}.
-Hint Mode TimelessP + ! : typeclass_instances.
+   format "[∗  mset]  x  ∈  X ,  P") : uPred_scope.
 
 (** * Properties *)
 Section big_op.
@@ -127,52 +36,6 @@ Context {M : ucmraT}.
 Implicit Types Ps Qs : list (uPred M).
 Implicit Types A : Type.
 
-Global Instance nil_persistent : PersistentL (@nil (uPred M)).
-Proof. constructor. Qed.
-Global Instance cons_persistent P Ps :
-  PersistentP P → PersistentL Ps → PersistentL (P :: Ps).
-Proof. by constructor. Qed.
-Global Instance app_persistent Ps Ps' :
-  PersistentL Ps → PersistentL Ps' → PersistentL (Ps ++ Ps').
-Proof. apply Forall_app_2. Qed.
-
-Global Instance fmap_persistent {A} (f : A → uPred M) xs :
-  (∀ x, PersistentP (f x)) → PersistentL (f <$> xs).
-Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
-Global Instance zip_with_persistent {A B} (f : A → B → uPred M) xs ys :
-  (∀ x y, PersistentP (f x y)) → PersistentL (zip_with f xs ys).
-Proof.
-  unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
-Qed.
-Global Instance imap_persistent {A} (f : nat → A → uPred M) xs :
-  (∀ i x, PersistentP (f i x)) → PersistentL (imap f xs).
-Proof. revert f. induction xs; simpl; constructor; naive_solver. Qed.
-
-(** ** Timelessness *)
-Global Instance big_sep_timeless Ps : TimelessL Ps → TimelessP ([∗] Ps).
-Proof. induction 1; apply _. Qed.
-
-Global Instance nil_timeless : TimelessL (@nil (uPred M)).
-Proof. constructor. Qed.
-Global Instance cons_timeless P Ps :
-  TimelessP P → TimelessL Ps → TimelessL (P :: Ps).
-Proof. by constructor. Qed.
-Global Instance app_timeless Ps Ps' :
-  TimelessL Ps → TimelessL Ps' → TimelessL (Ps ++ Ps').
-Proof. apply Forall_app_2. Qed.
-
-Global Instance fmap_timeless {A} (f : A → uPred M) xs :
-  (∀ x, TimelessP (f x)) → TimelessL (f <$> xs).
-Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
-Global Instance zip_with_timeless {A B} (f : A → B → uPred M) xs ys :
-  (∀ x y, TimelessP (f x y)) → TimelessL (zip_with f xs ys).
-Proof.
-  unfold TimelessL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
-Qed.
-Global Instance imap_timeless {A} (f : nat → A → uPred M) xs :
-  (∀ i x, TimelessP (f i x)) → TimelessL (imap f xs).
-Proof. revert f. induction xs; simpl; constructor; naive_solver. Qed.
-
 (** ** Big ops over lists *)
 Section list.
   Context {A : Type}.
@@ -203,14 +66,14 @@ Section list.
   Proof. apply big_opL_proper. Qed.
   Lemma big_sepL_submseteq (Φ : A → uPred M) l1 l2 :
     l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
-  Proof. intros ?. apply uPred_included. by apply: big_opL_submseteq. Qed.
+  Proof. intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l. Qed.
 
   Global Instance big_sepL_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
-           (big_opL (M:=uPredUR M) (A:=A)).
+           (big_opL (@uPred_sep M) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
   Global Instance big_sep_mono' :
-    Proper (Forall2 (⊢) ==> (⊢)) (big_opL (M:=uPredUR M) (λ _ P, P)).
+    Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@uPred_sep M) (λ _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
   Lemma big_sepL_lookup_acc Φ l i x :
@@ -224,11 +87,13 @@ Section list.
 
   Lemma big_sepL_lookup Φ l i x :
     l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x.
-  Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed.
+  Proof. intros. by rewrite big_sepL_lookup_acc // sep_elim_l. Qed.
 
   Lemma big_sepL_elem_of (Φ : A → uPred M) l x :
     x ∈ l → ([∗ list] y ∈ l, Φ y) ⊢ Φ x.
-  Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed.
+  Proof.
+    intros [i ?]%elem_of_list_lookup; eauto using (big_sepL_lookup (λ _, Φ)).
+  Qed.
 
   Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → uPred M) l :
     ([∗ list] k↦y ∈ f <$> l, Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k (f y)).
@@ -313,7 +178,7 @@ Section list2.
     ([∗ list] k↦x ∈ zip_with f l1 l2, Φ k x)
     ⊣⊢ ([∗ list] k↦x ∈ l1, ∀ y, ⌜l2 !! k = Some y⌝ → Φ k (f x y)).
   Proof.
-    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2]//.
+    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //.
     - apply (anti_symm _), True_intro.
       trans ([∗ list] _↦_ ∈ x :: l1, True : uPred M)%I.
       + rewrite big_sepL_forall. auto using forall_intro, impl_intro_l, True_intro.
@@ -346,7 +211,7 @@ Section gmap.
 
   Global Instance big_sepM_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
-           (big_opM (M:=uPredUR M) (A:=A)).
+           (big_opM (@uPred_sep M) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True.
@@ -357,12 +222,12 @@ Section gmap.
   Lemma big_sepM_insert Φ m i x :
     m !! i = None →
     ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ m, Φ k y.
-  Proof. apply: big_opM_insert. Qed.
+  Proof. apply big_opM_insert. Qed.
 
   Lemma big_sepM_delete Φ m i x :
     m !! i = Some x →
     ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y.
-  Proof. apply: big_opM_delete. Qed.
+  Proof. apply big_opM_delete. Qed.
 
   Lemma big_sepM_lookup_acc Φ m i x :
     m !! i = Some x →
@@ -373,7 +238,7 @@ Section gmap.
 
   Lemma big_sepM_lookup Φ m i x :
     m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x.
-  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed.
+  Proof. intros. by rewrite big_sepM_lookup_acc // sep_elim_l. Qed.
 
   Lemma big_sepM_lookup_dom (Φ : K → uPred M) m i :
     is_Some (m !! i) → ([∗ map] k↦_ ∈ m, Φ k) ⊢ Φ i.
@@ -389,7 +254,7 @@ Section gmap.
   Lemma big_sepM_insert_override Φ m i x x' :
     m !! i = Some x → (Φ i x ⊣⊢ Φ i x') →
     ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y) ⊣⊢ ([∗ map] k↦y ∈ m, Φ k y).
-  Proof. apply: big_opM_insert_override. Qed.
+  Proof. apply big_opM_insert_override. Qed.
 
   Lemma big_sepM_insert_override_1 Φ m i x x' :
     m !! i = Some x →
@@ -415,17 +280,17 @@ Section gmap.
     m !! i = None →
        ([∗ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     ⊣⊢ (Ψ i x b ∗ [∗ map] k↦y ∈ m, Ψ k y (f k)).
-  Proof. apply: big_opM_fn_insert. Qed.
+  Proof. apply big_opM_fn_insert. Qed.
 
   Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P :
     m !! i = None →
     ([∗ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ∗ [∗ map] k↦y ∈ m, Φ k).
-  Proof. apply: big_opM_fn_insert'. Qed.
+  Proof. apply big_opM_fn_insert'. Qed.
 
   Lemma big_sepM_sepM Φ Ψ m :
     ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x)
     ⊣⊢ ([∗ map] k↦x ∈ m, Φ k x) ∗ ([∗ map] k↦x ∈ m, Ψ k x).
-  Proof. apply: big_opM_opM. Qed.
+  Proof. apply big_opM_opM. Qed.
 
   Lemma big_sepM_and Φ Ψ m :
     ([∗ map] k↦x ∈ m, Φ k x ∧ Ψ k x)
@@ -507,10 +372,10 @@ Section gset.
   Lemma big_sepS_proper Φ Ψ X :
     (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) →
     ([∗ set] x ∈ X, Φ x) ⊣⊢ ([∗ set] x ∈ X, Ψ x).
-  Proof. apply: big_opS_proper. Qed.
+  Proof. apply big_opS_proper. Qed.
 
   Global Instance big_sepS_mono' :
-     Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (M:=uPredUR M) (A:=A)).
+     Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (@uPred_sep M) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ True.
@@ -520,29 +385,29 @@ Section gset.
 
   Lemma big_sepS_insert Φ X x :
     x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ∗ [∗ set] y ∈ X, Φ y).
-  Proof. apply: big_opS_insert. Qed.
+  Proof. apply big_opS_insert. Qed.
 
   Lemma big_sepS_fn_insert {B} (Ψ : A → B → uPred M) f X x b :
     x ∉ X →
        ([∗ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y))
     ⊣⊢ (Ψ x b ∗ [∗ set] y ∈ X, Ψ y (f y)).
-  Proof. apply: big_opS_fn_insert. Qed.
+  Proof. apply big_opS_fn_insert. Qed.
 
   Lemma big_sepS_fn_insert' Φ X x P :
     x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ∗ [∗ set] y ∈ X, Φ y).
-  Proof. apply: big_opS_fn_insert'. Qed.
+  Proof. apply big_opS_fn_insert'. Qed.
 
   Lemma big_sepS_union Φ X Y :
     X ⊥ Y →
     ([∗ set] y ∈ X ∪ Y, Φ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ Y, Φ y).
-  Proof. apply: big_opS_union. Qed.
+  Proof. apply big_opS_union. Qed.
 
   Lemma big_sepS_delete Φ X x :
     x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y.
-  Proof. apply: big_opS_delete. Qed.
+  Proof. apply big_opS_delete. Qed.
 
   Lemma big_sepS_elem_of Φ X x : x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x.
-  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
+  Proof. intros. rewrite big_sepS_delete //. auto with I. Qed.
 
   Lemma big_sepS_elem_of_acc Φ X x :
     x ∈ X →
@@ -552,7 +417,7 @@ Section gset.
   Qed.
 
   Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
-  Proof. apply: big_opS_singleton. Qed.
+  Proof. apply big_opS_singleton. Qed.
 
   Lemma big_sepS_filter (P : A → Prop) `{∀ x, Decision (P x)} Φ X :
     ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜P y⌝ → Φ y).
@@ -580,7 +445,7 @@ Section gset.
 
   Lemma big_sepS_sepS Φ Ψ X :
     ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y).
-  Proof. apply: big_opS_opS. Qed.
+  Proof. apply big_opS_opS. Qed.
 
   Lemma big_sepS_and Φ Ψ X :
     ([∗ set] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ set] y ∈ X, Φ y) ∧ ([∗ set] y ∈ X, Ψ y).
@@ -637,7 +502,7 @@ End gset.
 
 Lemma big_sepM_dom `{Countable K} {A} (Φ : K → uPred M) (m : gmap K A) :
   ([∗ map] k↦_ ∈ m, Φ k) ⊣⊢ ([∗ set] k ∈ dom _ m, Φ k).
-Proof. apply: big_opM_dom. Qed.
+Proof. apply big_opM_dom. Qed.
 
 
 (** ** Big ops over finite multisets *)
@@ -657,10 +522,10 @@ Section gmultiset.
   Lemma big_sepMS_proper Φ Ψ X :
     (∀ x, x ∈ X → Φ x ⊣⊢ Ψ x) →
     ([∗ mset] x ∈ X, Φ x) ⊣⊢ ([∗ mset] x ∈ X, Ψ x).
-  Proof. apply: big_opMS_proper. Qed.
+  Proof. apply big_opMS_proper. Qed.
 
   Global Instance big_sepMS_mono' :
-     Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opMS (M:=uPredUR M) (A:=A)).
+     Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opMS (@uPred_sep M) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_sepMS_empty Φ : ([∗ mset] x ∈ ∅, Φ x) ⊣⊢ True.
@@ -670,14 +535,14 @@ Section gmultiset.
 
   Lemma big_sepMS_union Φ X Y :
     ([∗ mset] y ∈ X ∪ Y, Φ y) ⊣⊢ ([∗ mset] y ∈ X, Φ y) ∗ [∗ mset] y ∈ Y, Φ y.
-  Proof. apply: big_opMS_union. Qed.
+  Proof. apply big_opMS_union. Qed.
 
   Lemma big_sepMS_delete Φ X x :
     x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ mset] y ∈ X ∖ {[ x ]}, Φ y.
-  Proof. apply: big_opMS_delete. Qed.
+  Proof. apply big_opMS_delete. Qed.
 
   Lemma big_sepMS_elem_of Φ X x : x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊢ Φ x.
-  Proof. intros. apply uPred_included. by apply: big_opMS_elem_of. Qed. 
+  Proof. intros. by rewrite big_sepMS_delete // sep_elim_l. Qed.
 
   Lemma big_sepMS_elem_of_acc Φ X x :
     x ∈ X →
@@ -687,11 +552,11 @@ Section gmultiset.
   Qed.
 
   Lemma big_sepMS_singleton Φ x : ([∗ mset] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
-  Proof. apply: big_opMS_singleton. Qed.
+  Proof. apply big_opMS_singleton. Qed.
 
   Lemma big_sepMS_sepMS Φ Ψ X :
     ([∗ mset] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ mset] y ∈ X, Φ y) ∗ ([∗ mset] y ∈ X, Ψ y).
-  Proof. apply: big_opMS_opMS. Qed.
+  Proof. apply big_opMS_opMS. Qed.
 
   Lemma big_sepMS_and Φ Ψ X :
     ([∗ mset] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ mset] y ∈ X, Φ y) ∧ ([∗ mset] y ∈ X, Ψ y).
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 43a753da3..80faccdea 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -889,5 +889,64 @@ Proof. intros. by rewrite /PersistentP always_ownM. Qed.
 Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
   (∀ x, PersistentP (Ψ x)) → PersistentP P → PersistentP (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
+
+(* For big ops *)
+Global Instance uPred_and_monoid : Monoid (@uPred_and M) :=
+  {| monoid_unit := True%I |}.
+Global Instance uPred_or_monoid : Monoid (@uPred_or M) :=
+  {| monoid_unit := False%I |}.
+Global Instance uPred_sep_monoid : Monoid (@uPred_sep M) :=
+  {| monoid_unit := True%I |}.
+
+Global Instance uPred_always_and_homomorphism :
+  MonoidHomomorphism uPred_and uPred_and (@uPred_always M).
+Proof. split; [split|]. apply _. apply always_and. apply always_pure. Qed.
+Global Instance uPred_always_if_and_homomorphism b :
+  MonoidHomomorphism uPred_and uPred_and (@uPred_always_if M b).
+Proof. split; [split|]. apply _. apply always_if_and. apply always_if_pure. Qed.
+Global Instance uPred_later_monoid_and_homomorphism :
+  MonoidHomomorphism uPred_and uPred_and (@uPred_later M).
+Proof. split; [split|]. apply _. apply later_and. apply later_True. Qed.
+Global Instance uPred_laterN_and_homomorphism n :
+  MonoidHomomorphism uPred_and uPred_and (@uPred_laterN M n).
+Proof. split; [split|]. apply _. apply laterN_and. apply laterN_True. Qed.
+Global Instance uPred_except_0_and_homomorphism :
+  MonoidHomomorphism uPred_and uPred_and (@uPred_except_0 M).
+Proof. split; [split|]. apply _. apply except_0_and. apply except_0_True. Qed.
+
+Global Instance uPred_always_or_homomorphism :
+  MonoidHomomorphism uPred_or uPred_or (@uPred_always M).
+Proof. split; [split|]. apply _. apply always_or. apply always_pure. Qed.
+Global Instance uPred_always_if_or_homomorphism b :
+  MonoidHomomorphism uPred_or uPred_or (@uPred_always_if M b).
+Proof. split; [split|]. apply _. apply always_if_or. apply always_if_pure. Qed.
+Global Instance uPred_later_monoid_or_homomorphism :
+  WeakMonoidHomomorphism uPred_or uPred_or (@uPred_later M).
+Proof. split. apply _. apply later_or. Qed.
+Global Instance uPred_laterN_or_homomorphism n :
+  WeakMonoidHomomorphism uPred_or uPred_or (@uPred_laterN M n).
+Proof. split. apply _. apply laterN_or. Qed.
+Global Instance uPred_except_0_or_homomorphism :
+  WeakMonoidHomomorphism uPred_or uPred_or (@uPred_except_0 M).
+Proof. split. apply _. apply except_0_or. Qed. 
+
+Global Instance uPred_always_sep_homomorphism :
+  MonoidHomomorphism uPred_sep uPred_sep (@uPred_always M).
+Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
+Global Instance uPred_always_if_sep_homomorphism b :
+  MonoidHomomorphism uPred_sep uPred_sep (@uPred_always_if M b).
+Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
+Global Instance uPred_later_monoid_sep_homomorphism :
+  MonoidHomomorphism uPred_sep uPred_sep (@uPred_later M).
+Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
+Global Instance uPred_laterN_sep_homomorphism n :
+  MonoidHomomorphism uPred_sep uPred_sep (@uPred_laterN M n).
+Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed.
+Global Instance uPred_except_0_sep_homomorphism :
+  MonoidHomomorphism uPred_sep uPred_sep (@uPred_except_0 M).
+Proof. split; [split|]. apply _. apply except_0_sep. apply except_0_True. Qed.
+Global Instance uPred_ownM_sep_homomorphism :
+  MonoidHomomorphism op uPred_sep (@uPred_ownM M).
+Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed.
 End derived.
 End uPred.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 460807788..0ae57d025 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -94,9 +94,10 @@ Section auth.
   Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
-
-  Global Instance auth_own_cmra_homomorphism : CMRAHomomorphism (auth_own γ).
+  Global Instance auth_own_sep_homomorphism γ :
+    WeakMonoidHomomorphism op uPred_sep (auth_own γ).
   Proof. split. apply _. apply auth_own_op. Qed.
+
   Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (auth_own γ).
   Proof. intros a1 a2. apply auth_own_mono. Qed.
 
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 9b9279f87..8e0b9d6d0 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -86,8 +86,6 @@ Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
 Lemma own_mono γ a1 a2 : a2 ≼ a1 → own γ a1 ⊢ own γ a2.
 Proof. move=> [c ->]. rewrite own_op. eauto with I. Qed.
 
-Global Instance own_cmra_homomorphism : CMRAHomomorphism (own γ).
-Proof. split. apply _. apply own_op. Qed.
 Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (@own Σ A _ γ).
 Proof. intros a1 a2. apply own_mono. Qed.
 
@@ -178,6 +176,11 @@ Proof.
   - intros x; destruct inG_prf. by rewrite left_id.
 Qed.
 
+(** Big op class instances *)
+Instance own_cmra_sep_homomorphism `{inG Σ (A:ucmraT)} :
+  WeakMonoidHomomorphism op uPred_sep (own γ).
+Proof. split. apply _. apply own_op. Qed.
+
 (** Proofmode class instances *)
 Section proofmode_classes.
   Context `{inG Σ A}.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 165cce17f..56bd2a267 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -67,8 +67,7 @@ Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
   iNext; iIntros (v2 σ2 efs) "%".
-  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst.
-  by iApply big_sepL_nil.
+  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
 Qed.
 
 Lemma wp_lift_pure_det_head_step {E E' Φ} e1 e2 efs :
@@ -86,7 +85,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {E E' Φ} e1 e2 :
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   (|={E,E'}▷=> WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}.
 Proof using Hinh.
-  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
+  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
 Qed.
 
 Lemma wp_lift_pure_det_head_step_no_fork' {E Φ} e1 e2 :
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index d94281cf3..fc96e4943 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -211,7 +211,7 @@ Section ectx_lifting.
     {{{ ▷ ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
   Proof.
     intros. rewrite -(ownP_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
-    rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
+    rewrite /= right_id. by apply uPred.wand_intro_r.
   Qed.
 
   Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
@@ -229,6 +229,6 @@ Section ectx_lifting.
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
   Proof using Hinh.
-    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
+    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
   Qed.
 End ectx_lifting.
-- 
GitLab