diff --git a/_CoqProject b/_CoqProject
index 784ef81cbc28358c6d7b066a8d4a0df5fea08a9b..fd5bd12a3797dc291f4c86a8f4bde4a006b42958 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/opam.pins b/opam.pins
index ee2d15f4df23e9a795c02d8d0eea4c6754bacab2..1b5b31d49c1a5dd9680f0cb3a987a575274a1196 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 0ac2b4db07bdc471421c5a4c47789087b3df074c
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp a0ce0937cfabe16a184af2d92c0466ebacecbca2
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index c673326ae19dff7f3679dc53dcdca72bf9a0da7d..536199c43e1231e04cf8db106849e231789b08d7 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 0000000000000000000000000000000000000000..26e043615bffcd9371be6017587d47d1d350de93
--- /dev/null
+++ b/theories/algebra/big_op.v
@@ -0,0 +1,494 @@
+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} _ !_ /.
+Typeclasses Opaque big_opL.
+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 eac3265ee6eb6ed35be8cbdf5b8db260a1706b73..d1556b415c0b18e8cb8722dc0bd78b087d2b2df8 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 206c3ac11af52b5e14249109239c8c3d5dd59884..54122de3ed8c1a25ea1f6be6af01daaff5a585e9 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -1,517 +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 *)
-(* This is the basic building block for other big ops *)
-Fixpoint big_op {M : ucmraT} (xs : list M) : M :=
-  match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
-Arguments big_op _ !_ /.
-Instance: Params (@big_op) 1.
-Notation "'[â‹…]' xs" := (big_op xs) (at level 20) : C_scope.
-
-(** * Other big ops *)
-Definition big_opL {M : ucmraT} {A} (l : list A) (f : nat → A → M) : M :=
-  [â‹…] (imap f l).
-Instance: Params (@big_opL) 2.
-Typeclasses Opaque big_opL.
-Notation "'[⋅' 'list' ] k ↦ x ∈ l , P" := (big_opL l (λ k x, P))
-  (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 l (λ _ x, P))
-  (at level 200, l at level 10, x at level 1, right associativity,
-   format "[⋅  list ]  x  ∈  l ,  P") : C_scope.
-
-Definition big_opM {M : ucmraT} `{Countable K} {A}
-    (m : gmap K A) (f : K → A → M) : M :=
-  [â‹…] (curry f <$> map_to_list m).
-Instance: Params (@big_opM) 6.
-Typeclasses Opaque big_opM.
-Notation "'[⋅' 'map' ] k ↦ x ∈ m , P" := (big_opM m (λ k x, P))
-  (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 m (λ _ x, P))
-  (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}
-  (X : gset A) (f : A → M) : M := [⋅] (f <$> elements X).
-Instance: Params (@big_opS) 5.
-Typeclasses Opaque big_opS.
-Notation "'[⋅' 'set' ] x ∈ X , P" := (big_opS X (λ x, P))
-  (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}
-  (X : gmultiset A) (f : A → M) : M := [⋅] (f <$> elements X).
-Instance: Params (@big_opMS) 5.
-Typeclasses Opaque big_opMS.
-Notation "'[⋅' 'mset' ] x ∈ X , P" := (big_opMS X (λ x, P))
-  (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 *)
-Lemma big_op_Forall2 R :
-  Reflexive R → Proper (R ==> R ==> R) (@op M _) →
-  Proper (Forall2 R ==> R) (@big_op M).
-Proof. rewrite /Proper /respectful. induction 3; eauto. Qed.
-
-Global Instance big_op_ne : NonExpansive (@big_op M).
-Proof. intros ?. apply big_op_Forall2; apply _. Qed.
-Global Instance big_op_proper : Proper ((≡) ==> (≡)) (@big_op M) := ne_proper _.
-
-Lemma big_op_nil : [⋅] (@nil M) = ∅.
-Proof. done. Qed.
-Lemma big_op_cons x xs : [â‹…] (x :: xs) = x â‹… [â‹…] xs.
-Proof. done. Qed.
-Lemma big_op_app xs ys : [⋅] (xs ++ ys) ≡ [⋅] xs ⋅ [⋅] ys.
-Proof.
-  induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
-  by rewrite IH assoc.
-Qed.
-
-Lemma big_op_mono xs ys : Forall2 (≼) xs ys → [⋅] xs ≼ [⋅] ys.
-Proof. induction 1 as [|x y xs ys Hxy ? IH]; simpl; eauto using cmra_mono. Qed.
-
-Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) (@big_op M).
-Proof.
-  induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
-  - by rewrite IH.
-  - by rewrite !assoc (comm _ x).
-  - by trans (big_op xs2).
-Qed.
-
-Lemma big_op_submseteq xs ys : xs ⊆+ ys → [⋅] xs ≼ [⋅] ys.
-Proof.
-  intros [xs' ->]%submseteq_Permutation.
-  rewrite big_op_app; apply cmra_included_l.
-Qed.
-
-Lemma big_op_delete xs i x : xs !! i = Some x → x ⋅ [⋅] delete i xs ≡ [⋅] xs.
-Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.
-
-Lemma big_sep_elem_of xs x : x ∈ xs → x ≼ [⋅] xs.
-Proof.
-  intros [i ?]%elem_of_list_lookup. rewrite -big_op_delete //.
-  apply cmra_included_l.
-Qed.
-
-(** ** 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. by rewrite /big_opL imap_cons. Qed.
-  Lemma big_opL_singleton f x : ([⋅ list] k↦y ∈ [x], f k y) ≡ f 0 x.
-  Proof. by rewrite big_opL_cons big_opL_nil 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. by rewrite /big_opL imap_app big_op_app. 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 ? Hop. revert f g. induction l as [|x l IH]=> f g Hf; [done|].
-    rewrite !big_opL_cons. apply Hop; 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. intros Hl. by rewrite /big_opL !imap_const Hl. Qed.
-  Lemma big_opL_submseteq (f : A → M) l1 l2 :
-    l1 ⊆+ l2 → ([⋅ list] x ∈ l1, f x) ≼ ([⋅ list] x ∈ l2, f x).
-  Proof. intros Hl. apply big_op_submseteq. rewrite !imap_const. by rewrite ->Hl. Qed.
-
-  Global Instance big_opL_ne l n :
-    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
-           (big_opL (M:=M) l).
-  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opL_proper' l :
-    Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡))
-           (big_opL (M:=M) l).
-  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opL_mono' l :
-    Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> (≼))
-           (big_opL (M:=M) l).
-  Proof. intros f g Hf. 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. by rewrite /big_opL imap_fmap. 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.
-    { by rewrite !big_opL_nil left_id. }
-    rewrite !big_opL_cons IH.
-    by rewrite -!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_op_Forall2 R _ _), Forall2_fmap, Forall_Forall2.
-    apply Forall_forall=> -[i x] ? /=. 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_op_submseteq, fmap_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 m n :
-    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
-           (big_opM (M:=M) m).
-  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opM_proper' m :
-    Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡))
-           (big_opM (M:=M) m).
-  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opM_mono' m :
-    Proper (pointwise_relation _ (pointwise_relation _ (≼)) ==> (≼))
-           (big_opM (M:=M) m).
-  Proof. intros f g Hf. 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 -list_fmap_compose.
-    f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
-  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.
-    induction m as [|i x ?? IH] using map_ind.
-    { by rewrite !big_opM_empty left_id. }
-    rewrite !big_opM_insert // IH.
-    by rewrite -!assoc (assoc _ (g _ _)) [(g _ _ â‹… _)]comm -!assoc.
-  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_op_Forall2 R _ _), Forall2_fmap, Forall_Forall2.
-    apply Forall_forall=> x ? /=. 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_op_submseteq, fmap_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 X n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X).
-  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opS_proper' X :
-    Proper (pointwise_relation _ (≡) ==> (≡)) (big_opS (M:=M) X).
-  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opS_mono' X :
-    Proper (pointwise_relation _ (≼) ==> (≼)) (big_opS (M:=M) X).
-  Proof. intros f g Hf. 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.
-    induction X as [|x X ? IH] using collection_ind_L.
-    { by rewrite !big_opS_empty left_id. }
-    rewrite !big_opS_insert // IH.
-    by rewrite -!assoc (assoc _ (g _)) [(g _ â‹… _)]comm -!assoc.
-  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_op_Forall2 R _ _), Forall2_fmap, Forall_Forall2.
-    apply Forall_forall=> x ? /=. 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_op_submseteq, fmap_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 X n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (big_opMS (M:=M) X).
-  Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opMS_proper' X :
-    Proper (pointwise_relation _ (≡) ==> (≡)) (big_opMS (M:=M) X).
-  Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_opMS_mono' X :
-    Proper (pointwise_relation _ (≼) ==> (≼)) (big_opMS (M:=M) X).
-  Proof. intros f g Hf. 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 fmap_app big_op_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.
-    induction X as [|x X IH] using gmultiset_ind.
-    { by rewrite !big_opMS_empty left_id. }
-    rewrite !big_opMS_union !big_opMS_singleton IH.
-    by rewrite -!assoc (assoc _ (g _)) [(g _ â‹… _)]comm -!assoc.
-  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 big_opL_cons op_None IH. split.
+  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.
@@ -521,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 !big_opL_nil ucmra_homomorphism_unit.
-  - by rewrite !big_opL_cons 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 a0d123cc4bc092d54c0248e3a134f7bb56322022..0000000000000000000000000000000000000000
--- 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 ≡ big_op ((λ n, from_option id ∅ (Σ !! n)) <$> flatten e).
-  Proof.
-    induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //.
-    by rewrite fmap_app IH1 IH2 big_op_app.
-  Qed.
-  Lemma flatten_correct Σ e1 e2 :
-    flatten e1 ⊆+ flatten e2 → eval Σ e1 ≼ eval Σ e2.
-  Proof.
-    by intros He; rewrite !eval_flatten; apply big_op_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 fedeab9db6f651d2fe1db9f9f714c2c3e6f7139b..1a786c352156c9174594b9ac7c302e772049e2ec 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 52b9e0ccc2c50f75564270cab0c6be7faf24ab68..77556eebd6406417f0308fb84e82b59fcca120e5 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 3b378c3db9675a4f8513b4918869f43dc9e40ef8..21d183d7833100f704c5540e887d0c00238727f3 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 0000000000000000000000000000000000000000..a9d11fbcbcb671236e32088cbdb0a29f2b86870c
--- /dev/null
+++ b/theories/algebra/monoid.v
@@ -0,0 +1,50 @@
+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;
+}.
+Lemma monoid_proper `{Monoid M o} : Proper ((≡) ==> (≡) ==> (≡)) o.
+Proof. apply ne_proper_2, monoid_ne. Qed.
+Lemma monoid_right_id `{Monoid M o} : RightId (≡) monoid_unit o.
+Proof. intros x. etrans; [apply monoid_comm|apply monoid_left_id]. Qed.
+
+(** The [Homomorphism] classes give rise to generic lemmas about big operators
+commuting with each other. We also consider a [WeakMonoidHomomorphism] which
+does not necesarrily commute with unit; an example is the [own] connective: we
+only have `True ==∗ own γ ∅`, not `True ↔ own γ ∅`. *)
+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 8dfa1f9830478f02324404cc9e89a6633cc938da..72b8e10d8b6f3d4dc7020536c5ace4c2023a8c0c 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -1,124 +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 "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
-
-Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P))
+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 _) l (λ _ x, P))
+   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 uPred_sep (λ _ x, x) Ps) (at level 20) : uPred_scope.
 
-Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P))
+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 _) m (λ _ x, P))
+   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 (λ x, P))
+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 (λ x, P))
+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.
@@ -126,74 +36,6 @@ Context {M : ucmraT}.
 Implicit Types Ps Qs : list (uPred M).
 Implicit Types A : Type.
 
-Global Instance big_sep_mono' :
-  Proper (Forall2 (⊢) ==> (⊢)) (big_op (M:=uPredUR M)).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-
-Lemma big_sep_app Ps Qs : [∗] (Ps ++ Qs) ⊣⊢ [∗] Ps ∗ [∗] Qs.
-Proof. by rewrite big_op_app. Qed.
-
-Lemma big_sep_submseteq Ps Qs : Qs ⊆+ Ps → [∗] Ps ⊢ [∗] Qs.
-Proof. intros. apply uPred_included. by apply: big_op_submseteq. Qed.
-Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P.
-Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
-Lemma big_sep_elem_of_acc Ps P : P ∈ Ps → [∗] Ps ⊢ P ∗ (P -∗ [∗] Ps).
-Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed.
-
-(** ** Persistence *)
-Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([∗] Ps).
-Proof. induction 1; apply _. Qed.
-
-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.
-  rewrite /PersistentL /imap=> ?. generalize 0. induction xs; constructor; auto.
-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.
-  rewrite /TimelessL /imap=> ?. generalize 0. induction xs; constructor; auto.
-Qed.
-
 (** ** Big ops over lists *)
 Section list.
   Context {A : Type}.
@@ -224,28 +66,34 @@ 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' l :
-    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
-           (big_opL (M:=uPredUR M) l).
-  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_sepL_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
+           (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 (@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 :
     l !! i = Some x →
     ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ list] k↦y ∈ l, Φ k y)).
   Proof.
-    intros Hli. apply big_sep_elem_of_acc, (elem_of_list_lookup_2 _ i).
-    by rewrite list_lookup_imap Hli.
+    intros Hli. rewrite -(take_drop_middle l i x) // big_sepL_app /=.
+    rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl.
+    rewrite assoc -!(comm _ (Φ _ _)) -assoc. by apply sep_mono_r, wand_intro_l.
   Qed.
 
   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)).
@@ -303,16 +151,21 @@ Section list.
 
   Global Instance big_sepL_nil_persistent Φ :
     PersistentP ([∗ list] k↦x ∈ [], Φ k x).
-  Proof. rewrite /big_opL. apply _. Qed.
+  Proof. simpl; apply _. Qed.
   Global Instance big_sepL_persistent Φ l :
     (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ list] k↦x ∈ l, Φ k x).
-  Proof. rewrite /big_opL. apply _. Qed.
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Global Instance big_sepL_persistent_id Ps : PersistentL Ps → PersistentP ([∗] Ps).
+  Proof. induction 1; simpl; apply _. Qed.
+
   Global Instance big_sepL_nil_timeless Φ :
     TimelessP ([∗ list] k↦x ∈ [], Φ k x).
-  Proof. rewrite /big_opL. apply _. Qed.
+  Proof. simpl; apply _. Qed.
   Global Instance big_sepL_timeless Φ l :
     (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ list] k↦x ∈ l, Φ k x).
-  Proof. rewrite /big_opL. apply _. Qed.
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Global Instance big_sepL_timeless_id Ps : TimelessL Ps → TimelessP ([∗] Ps).
+  Proof. induction 1; simpl; apply _. Qed.
 End list.
 
 Section list2.
@@ -325,13 +178,13 @@ 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]//=.
-    - rewrite big_sepL_nil. apply (anti_symm _), True_intro.
+    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.
       + apply big_sepL_mono=> k y _. apply forall_intro=> z.
         by apply impl_intro_l, pure_elim_l.
-    - rewrite !big_sepL_cons IH. apply sep_proper=> //. apply (anti_symm _).
+    - rewrite /= IH. apply sep_proper=> //. apply (anti_symm _).
       + apply forall_intro=>z /=. by apply impl_intro_r, pure_elim_r=>-[->].
       + rewrite (forall_elim y) /=. by eapply impl_elim, pure_intro.
   Qed.
@@ -348,8 +201,7 @@ Section gmap.
     ([∗ map] k ↦ x ∈ m1, Φ k x) ⊢ [∗ map] k ↦ x ∈ m2, Ψ k x.
   Proof.
     intros Hm HΦ. trans ([∗ map] k↦x ∈ m2, Φ k x)%I.
-    - apply uPred_included. apply: big_op_submseteq.
-      by apply fmap_submseteq, map_to_list_submseteq.
+    - rewrite /big_opM. by apply big_sepL_submseteq, map_to_list_submseteq.
     - apply big_opM_forall; apply _ || auto.
   Qed.
   Lemma big_sepM_proper Φ Ψ m :
@@ -357,10 +209,10 @@ Section gmap.
     ([∗ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([∗ map] k ↦ x ∈ m, Ψ k x).
   Proof. apply big_opM_proper. Qed.
 
-  Global Instance big_sepM_mono' m :
-    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
-           (big_opM (M:=uPredUR M) m).
-  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_sepM_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
+           (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.
   Proof. by rewrite big_opM_empty. Qed.
@@ -370,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 →
@@ -386,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.
@@ -402,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 →
@@ -428,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)
@@ -493,13 +345,13 @@ Section gmap.
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_persistent Φ m :
     (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ map] k↦x ∈ m, Φ k x).
-  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
+  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
   Global Instance big_sepM_nil_timeless Φ :
     TimelessP ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_timeless Φ m :
     (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ map] k↦x ∈ m, Φ k x).
-  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
+  Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
 End gmap.
 
 
@@ -514,18 +366,17 @@ Section gset.
     ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ Y, Ψ x.
   Proof.
     intros HX HΦ. trans ([∗ set] x ∈ Y, Φ x)%I.
-    - apply uPred_included. apply: big_op_submseteq.
-      by apply fmap_submseteq, elements_submseteq.
+    - rewrite /big_opM. by apply big_sepL_submseteq, elements_submseteq.
     - apply big_opS_forall; apply _ || auto.
   Qed.
   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' X :
-     Proper (pointwise_relation _ (⊢) ==> (⊢)) (big_opS (M:=uPredUR M) X).
-  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_sepS_mono' :
+     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.
   Proof. by rewrite big_opS_empty. Qed.
@@ -534,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 →
@@ -566,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).
@@ -594,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).
@@ -651,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 *)
@@ -665,18 +516,17 @@ Section gmultiset.
     ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Ψ x.
   Proof.
     intros HX HΦ. trans ([∗ mset] x ∈ Y, Φ x)%I.
-    - apply uPred_included. apply: big_op_submseteq.
-      by apply fmap_submseteq, gmultiset_elements_submseteq.
+    - rewrite /big_opM. by apply big_sepL_submseteq, gmultiset_elements_submseteq.
     - apply big_opMS_forall; apply _ || auto.
   Qed.
   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' X :
-     Proper (pointwise_relation _ (⊢) ==> (⊢)) (big_opMS (M:=uPredUR M) X).
-  Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
+  Global Instance big_sepMS_mono' :
+     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.
   Proof. by rewrite big_opMS_empty. Qed.
@@ -685,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 →
@@ -702,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 43a753da34d3f0116e52c7a68e12b7aa57f79e78..80faccdeabad9d150177f2fe93ab5efe9c74dab4 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 460807788bf5ae4bce7879b4ab6a67a0a4ef5395..0ae57d025fe93ecdf0d158e556eab9802f97b72d 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/boxes.v b/theories/base_logic/lib/boxes.v
index 5104c7f901f2267e23c304c2ce5400c08bd666b3..4151452bc6c50490c1cd8aa7ee9a2ff5d4a19694 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -97,9 +97,8 @@ Qed.
 
 Lemma box_alloc : box N ∅ True%I.
 Proof.
-  iIntros; iExists (λ _, True)%I; iSplit.
-  - iNext. by rewrite big_sepM_empty.
-  - by rewrite big_sepM_empty.
+  iIntros; iExists (λ _, True)%I; iSplit; last done.
+  iNext. by rewrite big_opM_empty.
 Qed.
 
 Lemma slice_insert_empty E q f Q P :
@@ -116,8 +115,8 @@ Proof.
   { iNext. iExists false; eauto. }
   iModIntro; iExists γ; repeat iSplit; auto.
   iNext. iExists (<[γ:=Q]> Φ); iSplit.
-  - iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'.
-  - rewrite (big_sepM_fn_insert (λ _ _ P',  _ ∗ _ _ P' ∗ _ _ (_ _ P')))%I //.
+  - iNext. iRewrite "HeqP". by rewrite big_opM_fn_insert'.
+  - rewrite (big_opM_fn_insert (λ _ _ P',  _ ∗ _ _ P' ∗ _ _ (_ _ P')))%I //.
     iFrame; eauto.
 Qed.
 
@@ -130,13 +129,13 @@ Proof.
   iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
   iInv N as (b) "[>Hγ _]" "Hclose".
-  iDestruct (big_sepM_delete _ f _ false with "Hf")
+  iDestruct (big_opM_delete _ f _ false with "Hf")
     as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
   iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
   iMod ("Hclose" with "[Hγ]"); first iExists false; eauto.
   iModIntro. iNext. iSplit.
   - iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
-    iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_sepM_delete.
+    iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete.
   - iExists Φ; eauto.
 Qed.
 
@@ -147,13 +146,13 @@ Lemma slice_fill E q f γ P Q :
 Proof.
   iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iInv N as (b') "[>Hγ _]" "Hclose".
-  iDestruct (big_sepM_delete _ f _ false with "Hf")
+  iDestruct (big_opM_delete _ f _ false with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
   iMod ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
   iModIntro; iNext; iExists Φ; iSplit.
-  - by rewrite big_sepM_insert_override.
-  - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
+  - by rewrite big_opM_insert_override.
+  - rewrite -insert_delete big_opM_insert ?lookup_delete //.
     iFrame; eauto.
 Qed.
 
@@ -164,15 +163,15 @@ Lemma slice_empty E q f P Q γ :
 Proof.
   iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iInv N as (b) "[>Hγ HQ]" "Hclose".
-  iDestruct (big_sepM_delete _ f with "Hf")
+  iDestruct (big_opM_delete _ f with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
   iFrame "HQ".
   iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
   iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
   iModIntro; iNext; iExists Φ; iSplit.
-  - by rewrite big_sepM_insert_override.
-  - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
+  - by rewrite big_opM_insert_override.
+  - rewrite -insert_delete big_opM_insert ?lookup_delete //.
     iFrame; eauto.
 Qed.
 
@@ -205,11 +204,11 @@ Lemma box_fill E f P :
   box N f P -∗ ▷ P ={E}=∗ box N (const true <$> f) P.
 Proof.
   iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
-  iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
-  rewrite internal_eq_iff later_iff big_sepM_later.
+  iExists Φ; iSplitR; first by rewrite big_opM_fmap.
+  rewrite internal_eq_iff later_iff big_opM_commute.
   iDestruct ("HeqP" with "HP") as "HP".
   iCombine "Hf" "HP" as "Hf".
-  rewrite -big_sepM_sepM big_sepM_fmap; iApply (fupd_big_sepM _ _ f).
+  rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
   iApply (@big_sepM_impl with "[$Hf]").
   iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
   iInv N as (b) "[>Hγ _]" "Hclose".
@@ -226,7 +225,7 @@ Proof.
   iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ) ∗
     [∗ map] γ↦b ∈ f, box_own_auth γ (◯ Excl' false) ∗  box_own_prop γ (Φ γ) ∗
       inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
-  { rewrite -big_sepM_sepM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
+  { rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
     iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
     assert (true = b) as <- by eauto.
     iInv N as (b) "[>Hγ HΦ]" "Hclose".
@@ -235,8 +234,8 @@ Proof.
     iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
     iFrame "HγΦ Hinv". by iApply "HΦ". }
   iModIntro; iSplitL "HΦ".
-  - rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".
-  - iExists Φ; iSplit; by rewrite big_sepM_fmap.
+  - rewrite internal_eq_iff later_iff big_opM_commute. by iApply "HeqP".
+  - iExists Φ; iSplit; by rewrite big_opM_fmap.
 Qed.
 
 Lemma slice_iff E q f P Q Q' γ b :
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index 1353729f4ed222976bdc441787b3bd611199e1dc..a94ea6989ed1ee7caf9790a6215928d8e3c639f7 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -63,30 +63,22 @@ Section fractional.
   Global Instance fractional_big_sepL {A} l Ψ :
     (∀ k (x : A), Fractional (Ψ k x)) →
     Fractional (M:=M) (λ q, [∗ list] k↦x ∈ l, Ψ k x q)%I.
-  Proof.
-    intros ? q q'. rewrite -big_sepL_sepL. by setoid_rewrite fractional.
-  Qed.
+  Proof. intros ? q q'. rewrite -big_opL_opL. by setoid_rewrite fractional. Qed.
 
   Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
     (∀ k (x : A), Fractional (Ψ k x)) →
     Fractional (M:=M) (λ q, [∗ map] k↦x ∈ m, Ψ k x q)%I.
-  Proof.
-    intros ? q q'. rewrite -big_sepM_sepM. by setoid_rewrite fractional.
-  Qed.
+  Proof. intros ? q q'. rewrite -big_opM_opM. by setoid_rewrite fractional. Qed.
 
   Global Instance fractional_big_sepS `{Countable A} (X : gset A) Ψ :
     (∀ x, Fractional (Ψ x)) →
     Fractional (M:=M) (λ q, [∗ set] x ∈ X, Ψ x q)%I.
-  Proof.
-    intros ? q q'. rewrite -big_sepS_sepS. by setoid_rewrite fractional.
-  Qed.
+  Proof. intros ? q q'. rewrite -big_opS_opS. by setoid_rewrite fractional. Qed.
 
   Global Instance fractional_big_sepMS `{Countable A} (X : gmultiset A) Ψ :
     (∀ x, Fractional (Ψ x)) →
     Fractional (M:=M) (λ q, [∗ mset] x ∈ X, Ψ x q)%I.
-  Proof.
-    intros ? q q'. rewrite -big_sepMS_sepMS. by setoid_rewrite fractional.
-  Qed.
+  Proof. intros ? q q'. rewrite -big_opMS_opMS. by setoid_rewrite fractional. Qed.
 
   (** Mult instances *)
 
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 9b9279f878e382fabe6b1e3293ef06ad627b6760..8e0b9d6d024f46b82d53778e0cbd414130e43808 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/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index ced2ab68ca2612b5d995e29799a53f8728df7e6b..3fc0558cb6af3ca95fee23f955e4a676c644a3a8 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -105,9 +105,9 @@ Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ow
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
   iDestruct (invariant_lookup I i P with "[$]") as (Q) "[% #HPQ]".
-  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
+  iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
-    iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
+    iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
     iFrame "HI"; eauto.
   - iDestruct (ownE_singleton_twice with "[$HiE $HiE']") as %[].
 Qed.
@@ -115,9 +115,9 @@ Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ o
 Proof.
   rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
   iDestruct (invariant_lookup with "[$]") as (Q) "[% #HPQ]".
-  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
+  iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
   - iDestruct (ownD_singleton_twice with "[$]") as %[].
-  - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
+  - iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
     iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
 Qed.
 
@@ -139,7 +139,7 @@ Proof.
   iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
   iExists (<[i:=P]>I); iSplitL "Hw".
   { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
-  iApply (big_sepM_insert _ I); first done.
+  iApply (big_opM_insert _ I); first done.
   iFrame "HI". iLeft. by rewrite /ownD; iFrame.
 Qed.
 
@@ -162,7 +162,7 @@ Proof.
   rewrite -/(ownD _). iFrame "HD".
   iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
   { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
-  iApply (big_sepM_insert _ I); first done.
+  iApply (big_opM_insert _ I); first done.
   iFrame "HI". by iRight.
 Qed.
 End wsat.
diff --git a/theories/base_logic/tactics.v b/theories/base_logic/tactics.v
index 0a75c4fb55477da496025bcbe936d97f0116f86d..717bcec14f9d80be7a7455ff8b6d90edc8eb45a7 100644
--- a/theories/base_logic/tactics.v
+++ b/theories/base_logic/tactics.v
@@ -23,17 +23,16 @@ Module uPred_reflection. Section uPred_reflection.
     | ESep e1 e2 => flatten e1 ++ flatten e2
     end.
 
-  Notation eval_list Σ l := ([∗] ((λ n, from_option id True%I (Σ !! n)) <$> l))%I.
+  Notation eval_list Σ l := ([∗ list] n ∈ l, from_option id True (Σ !! n))%I.
+
   Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
   Proof.
     induction e as [| |e1 IH1 e2 IH2];
-      rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //. 
+      rewrite /= ?right_id ?big_opL_app ?IH1 ?IH2 //.
   Qed.
   Lemma flatten_entails Σ e1 e2 :
     flatten e2 ⊆+ flatten e1 → eval Σ e1 ⊢ eval Σ e2.
-  Proof.
-    intros. rewrite !eval_flatten. by apply big_sep_submseteq, fmap_submseteq.
-  Qed.
+  Proof. intros. rewrite !eval_flatten. by apply big_sepL_submseteq. Qed.
   Lemma flatten_equiv Σ e1 e2 :
     flatten e2 ≡ₚ flatten e1 → eval Σ e1 ⊣⊢ eval Σ e2.
   Proof. intros He. by rewrite !eval_flatten He. Qed.
@@ -90,7 +89,7 @@ Module uPred_reflection. Section uPred_reflection.
   Proof.
     intros ??. rewrite !eval_flatten.
     rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
-    rewrite !fmap_app !big_sep_app. apply sep_mono_r.
+    rewrite !big_opL_app. apply sep_mono_r.
   Qed.
 
   Fixpoint to_expr (l : list nat) : expr :=
@@ -110,7 +109,7 @@ Module uPred_reflection. Section uPred_reflection.
     cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ (to_expr ns) ∗ eval Σ e').
   Proof.
     intros He%flatten_cancel.
-    by rewrite eval_flatten He fmap_app big_sep_app eval_to_expr eval_flatten.
+    by rewrite eval_flatten He big_opL_app eval_to_expr eval_flatten.
   Qed.
   Lemma split_r Σ e ns e' :
     cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ e' ∗ eval Σ (to_expr ns)).
diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index d06424595a0662baf2ca43593fca19603e348f0e..f02b1078bff51a120d8077bf20b2afa5e3fa9a06 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -76,15 +76,15 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
   ress P ({[i1;i2]} ∪ I ∖ {[i]}).
 Proof.
   iIntros (????) "#HQ #H1 #H2 HQR"; iDestruct 1 as (Ψ) "[HPΨ HΨ]".
-  iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
+  iDestruct (big_opS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
   iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
   - iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
     iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
-    iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
+    iDestruct (big_opS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
     iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
-    rewrite -assoc_L !big_sepS_fn_insert'; [|abstract set_solver ..].
+    rewrite -assoc_L !big_opS_fn_insert'; [|abstract set_solver ..].
     by iFrame.
-  - rewrite -assoc_L !big_sepS_fn_insert; [|abstract set_solver ..]. eauto.
+  - rewrite -assoc_L !big_opS_fn_insert; [|abstract set_solver ..]. eauto.
 Qed.
 
 (** Actual proofs *)
@@ -98,7 +98,7 @@ Proof.
   iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
     as (γ') "[#? Hγ']"; eauto.
   { iNext. rewrite /barrier_inv /=. iFrame.
-    iExists (const P). rewrite !big_sepS_singleton /=. eauto. }
+    iExists (const P). rewrite !big_opS_singleton /=. eauto. }
   iAssert (barrier_ctx γ' l P)%I as "#?".
   { done. }
   iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
@@ -147,9 +147,9 @@ Proof.
   - (* a High state: the comparison succeeds, and we perform a transition and
     return to the client *)
     iDestruct "Hr" as (Ψ) "[HΨ Hsp]".
-    iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
+    iDestruct (big_opS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
     iAssert (▷ Ψ i ∗ ▷ [∗ set] j ∈ I ∖ {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
-    { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
+    { iNext. iApply (big_opS_delete _ _ i); first done. by iApply "HΨ". }
     iMod ("Hclose" $! (State High (I ∖ {[ i ]})) (∅ : set token) with "[HΨ' Hl Hsp]").
     { iSplit; [iPureIntro; by eauto using wait_step|].
       rewrite /barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 9de570086bb2cd94928159d888e15650f54e0067..7368ecf3d581934b9e659bad700133de90a4aae0 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -76,7 +76,7 @@ Lemma wp_fork E e Φ :
   ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
+  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ (Lit _)) // right_id.
   - intros; inv_head_step; eauto.
 Qed.
 
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 1227a421976d4430e25d3d29c74b5aaaf8e69c13..0618e26c5b0ff6ffafacc54b255712b578bee5cf 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -30,7 +30,7 @@ Proof.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
   iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
   rewrite /wsat /ownE; iFrame.
-  iExists ∅. rewrite fmap_empty big_sepM_empty. by iFrame.
+  iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
 Qed.
 
 (* Program logic adequacy *)
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 165cce17f4dfedecdde83dd246e59465e1ce0a69..56bd2a2674af965d874457af220f6c99e14e5dfe 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 d94281cf33ed21892f6c0e2d645f1d2ca4e90001..fc96e4943edf91e68e8bc976a31ff8dcba8abcb4 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.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index a4829ce47f905c49c3797bc03aa44f0be6124bed..b5176725dfeb0dcb969e69dd0e15d3f286140d1a 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -181,7 +181,7 @@ Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat → A → uPred M) (l: l
   IntoLaterN' n ([∗ list] k ↦ x ∈ l, Φ k x) ([∗ list] k ↦ x ∈ l, Ψ k x).
 Proof.
   rewrite /IntoLaterN' /IntoLaterN=> ?.
-  rewrite big_sepL_laterN. by apply big_sepL_mono.
+  rewrite big_opL_commute. by apply big_sepL_mono.
 Qed.
 Global Instance into_laterN_big_sepM n `{Countable K} {A}
     (Φ Ψ : K → A → uPred M) (m : gmap K A) :
@@ -189,7 +189,7 @@ Global Instance into_laterN_big_sepM n `{Countable K} {A}
   IntoLaterN' n ([∗ map] k ↦ x ∈ m, Φ k x) ([∗ map] k ↦ x ∈ m, Ψ k x).
 Proof.
   rewrite /IntoLaterN' /IntoLaterN=> ?.
-  rewrite big_sepM_laterN; by apply big_sepM_mono.
+  rewrite big_opM_commute; by apply big_sepM_mono.
 Qed.
 Global Instance into_laterN_big_sepS n `{Countable A}
     (Φ Ψ : A → uPred M) (X : gset A) :
@@ -197,7 +197,7 @@ Global Instance into_laterN_big_sepS n `{Countable A}
   IntoLaterN' n ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ x).
 Proof.
   rewrite /IntoLaterN' /IntoLaterN=> ?.
-  rewrite big_sepS_laterN; by apply big_sepS_mono.
+  rewrite big_opS_commute; by apply big_sepS_mono.
 Qed.
 Global Instance into_laterN_big_sepMS n `{Countable A}
     (Φ Ψ : A → uPred M) (X : gmultiset A) :
@@ -205,7 +205,7 @@ Global Instance into_laterN_big_sepMS n `{Countable A}
   IntoLaterN' n ([∗ mset] x ∈ X, Φ x) ([∗ mset] x ∈ X, Ψ x).
 Proof.
   rewrite /IntoLaterN' /IntoLaterN=> ?.
-  rewrite big_sepMS_laterN; by apply big_sepMS_mono.
+  rewrite big_opMS_commute; by apply big_sepMS_mono.
 Qed.
 
 (* FromLater *)
@@ -354,7 +354,7 @@ Proof. intros. by rewrite /FromAnd big_opL_cons always_and_sep_l. Qed.
 Global Instance from_and_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 :
   FromAnd false ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
-Proof. by rewrite /FromAnd big_sepL_app. Qed.
+Proof. by rewrite /FromAnd big_opL_app. Qed.
 Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M) l1 l2 :
   (∀ k y, PersistentP (Φ k y)) →
   FromAnd true ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
@@ -483,7 +483,7 @@ Global Instance frame_big_sepL_app {A} p (Φ : nat → A → uPred M) R Q l l1 l
   Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
            [∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
   Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
-Proof. rewrite /IsApp=>->. by rewrite /Frame big_sepL_app. Qed.
+Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
 
 Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ.
 Global Instance make_and_true_l P : MakeAnd True P P.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 29272ebc49ced480907431fe2e918b16ca289f68..ad39f0c34e7dc7f90aad13f7870fe902977f0ac1 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -234,14 +234,14 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
     + rewrite (env_app_perm _ _ Γp') //.
-      rewrite big_sep_app always_sep. solve_sep_entails.
+      rewrite big_opL_app always_sep. solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using env_app_wf.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
-    + rewrite (env_app_perm _ _ Γs') // big_sep_app. solve_sep_entails.
+    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
 Qed.
 
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
@@ -257,14 +257,14 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
     + rewrite (env_replace_perm _ _ Γp') //.
-      rewrite big_sep_app always_sep. solve_sep_entails.
+      rewrite big_opL_app always_sep. solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
-    + rewrite (env_replace_perm _ _ Γs') // big_sep_app. solve_sep_entails.
+    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
 Qed.
 
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :