diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index d7f86c27dffb69ce6d0468d45c3b8182c37a8d94..7bf52ebc2d90a1bb6b37f59afb9d85c6563752cd 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -101,23 +101,36 @@ Section list.
   Lemma big_opL_unit l : ([^o list] kâ†¦y âˆˆ l, monoid_unit) â‰¡ (monoid_unit : M).
   Proof. induction l; rewrite /= ?left_id //. Qed.
 
-  Lemma big_opL_forall R f g l :
+  Lemma big_opL_gen_proper_2 (R : relation M) f g l1 l2 :
+    R monoid_unit monoid_unit â†’
+    Proper (R ==> R ==> R) o â†’
+    (âˆ€ k,
+      match l1 !! k, l2 !! k with
+      | Some y1, Some y2 => R (f k y1) (g k y2)
+      | None, None => True
+      | _, _ => False
+      end) â†’
+    R ([^o list] k â†¦ y âˆˆ l1, f k y) ([^o list] k â†¦ y âˆˆ l2, g k y).
+  Proof.
+    intros ??. revert l2 f g. induction l1 as [|x1 l1 IH]=> -[|x2 l2] //= f g Hfg.
+    - by specialize (Hfg 0).
+    - by specialize (Hfg 0).
+    - f_equiv; [apply (Hfg 0)|]. apply IH. intros k. apply (Hfg (S k)).
+  Qed.
+  Lemma big_opL_gen_proper 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.
+    intros. apply big_opL_gen_proper_2; [done..|].
+    intros k. destruct (l !! k) eqn:?; auto.
   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.
+  Proof. apply big_opL_gen_proper; 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).
@@ -131,14 +144,41 @@ Section list.
     Proper ((â‰¡â‚š) ==> (â‰¡)) (big_opL o (Î» _, f)).
   Proof. intros xs1 xs2. apply big_opL_permutation. Qed.
 
-  Global Instance big_opL_ne n :
+  (** The lemmas [big_opL_ne] and [big_opL_proper] are more generic than the
+  instances as they also give [l !! k = Some y] in the premise. *)
+  Lemma big_opL_ne f g l n :
+    (âˆ€ k y, l !! k = Some y â†’ f k y â‰¡{n}â‰¡ g k y) â†’
+    ([^o list] k â†¦ y âˆˆ l, f k y) â‰¡{n}â‰¡ ([^o list] k â†¦ y âˆˆ l, g k y).
+  Proof. apply big_opL_gen_proper; 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_gen_proper; apply _. Qed.
+
+  (** The version [big_opL_proper_2] with [â‰¡] for the list arguments can only be
+  used if there is a setoid on [A]. The version for [dist n] can be found in
+  [algebra.list]. We do not define this lemma as a [Proper] instance, since
+  [f_equiv] will then use sometimes use this one, and other times
+  [big_opL_proper'], depending on whether a setoid on [A] exists. *)
+  Lemma big_opL_proper_2 `{!Equiv A} f g l1 l2 :
+    l1 â‰¡ l2 â†’
+    (âˆ€ k y1 y2,
+      l1 !! k = Some y1 â†’ l2 !! k = Some y2 â†’ y1 â‰¡ y2 â†’ f k y1 â‰¡ g k y2) â†’
+    ([^o list] k â†¦ y âˆˆ l1, f k y) â‰¡ ([^o list] k â†¦ y âˆˆ l2, g k y).
+  Proof.
+    intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
+    intros k. assert (l1 !! k â‰¡ l2 !! k) as Hlk by (by f_equiv).
+    destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
+  Qed.
+
+  Global Instance big_opL_ne' n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (=) ==> dist n)
            (big_opL o (A:=A)).
-  Proof. intros f f' Hf l ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
+  Proof. intros f f' Hf l ? <-. apply big_opL_ne; intros; apply Hf. Qed.
   Global Instance big_opL_proper' :
     Proper (pointwise_relation _ (pointwise_relation _ (â‰¡)) ==> (=) ==> (â‰¡))
            (big_opL o (A:=A)).
-  Proof. intros f f' Hf l ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
+  Proof. intros f f' Hf l ? <-. apply big_opL_proper; 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.
@@ -172,48 +212,96 @@ Section gmap.
   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 â†’
+  Lemma big_opM_empty f : ([^o map] kâ†¦x âˆˆ âˆ…, f k x) = monoid_unit.
+  Proof. by rewrite big_opM_eq /big_opM_def 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_eq /big_opM_def 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_gen_proper_2 (R : relation M) f g m1 m2 :
+    subrelation (â‰¡) R â†’ Equivalence R â†’
+    Proper (R ==> R ==> R) o â†’
+    (âˆ€ k,
+      match m1 !! k, m2 !! k with
+      | Some y1, Some y2 => R (f k y1) (g k y2)
+      | None, None => True
+      | _, _ => False
+      end) â†’
+    R ([^o map] k â†¦ x âˆˆ m1, f k x) ([^o map] k â†¦ x âˆˆ m2, g k x).
+  Proof.
+    intros HR ??. revert m2 f g.
+    induction m1 as [|k x1 m1 Hm1k IH] using map_ind=> m2 f g Hfg.
+    { destruct m2 as [|k x2 m2 _ _] using map_ind.
+      { rewrite !big_opM_empty. by apply HR. }
+      generalize (Hfg k). by rewrite lookup_empty lookup_insert. }
+    generalize (Hfg k). rewrite lookup_insert.
+    destruct (m2 !! k) as [x2|] eqn:Hm2k; [intros Hk|done].
+    etrans; [by apply HR, big_opM_insert|].
+    etrans; [|by symmetry; apply HR, big_opM_delete].
+    f_equiv; [done|]. apply IH=> k'. destruct (decide (k = k')) as [->|?].
+    - by rewrite lookup_delete Hm1k.
+    - generalize (Hfg k'). rewrite lookup_insert_ne // lookup_delete_ne //.
+  Qed.
+
+  Lemma big_opM_gen_proper 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. rewrite big_opM_eq. apply (big_opL_forall R); auto.
+    intros ?? Hf. rewrite big_opM_eq. apply (big_opL_gen_proper 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.
+  Proof. apply big_opM_gen_proper; apply _. Qed.
+
+  (** The lemmas [big_opM_ne] and [big_opM_proper] are more generic than the
+  instances as they also give [m !! k = Some y] in the premise. *)
+  Lemma big_opM_ne f g m n :
+    (âˆ€ k x, m !! k = Some x â†’ f k x â‰¡{n}â‰¡ g k x) â†’
+    ([^o map] k â†¦ x âˆˆ m, f k x) â‰¡{n}â‰¡ ([^o map] k â†¦ x âˆˆ m, g k x).
+  Proof. apply big_opM_gen_proper; 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.
+  Proof. apply big_opM_gen_proper; apply _. Qed.
+  (** The version [big_opL_proper_2] with [â‰¡] for the map arguments can only be
+  used if there is a setoid on [A]. The version for [dist n] can be found in
+  [algebra.gmap]. We do not define this lemma as a [Proper] instance, since
+  [f_equiv] will then use sometimes use this one, and other times
+  [big_opM_proper'], depending on whether a setoid on [A] exists. *)
+  Lemma big_opM_proper_2 `{!Equiv A} f g m1 m2 :
+    m1 â‰¡ m2 â†’
+    (âˆ€ k y1 y2,
+      m1 !! k = Some y1 â†’ m2 !! k = Some y2 â†’ y1 â‰¡ y2 â†’ f k y1 â‰¡ g k y2) â†’
+    ([^o map] k â†¦ y âˆˆ m1, f k y) â‰¡ ([^o map] k â†¦ y âˆˆ m2, g k y).
+  Proof.
+    intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
+    intros k. assert (m1 !! k â‰¡ m2 !! k) as Hlk by (by f_equiv).
+    destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
+  Qed.
 
-  Global Instance big_opM_ne n :
+  Global Instance big_opM_ne' n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (=) ==> dist n)
            (big_opM o (K:=K) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
+  Proof. intros f g Hf m ? <-. apply big_opM_ne; intros; apply Hf. Qed.
   Global Instance big_opM_proper' :
     Proper (pointwise_relation _ (pointwise_relation _ (â‰¡)) ==> (=) ==> (â‰¡))
            (big_opM o (K:=K) (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_eq /big_opM_def 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_eq /big_opM_def 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.
+  Proof. intros f g Hf m ? <-. apply big_opM_proper; intros; apply Hf. Qed.
 
   Lemma big_opM_singleton f i x : ([^o map] kâ†¦y âˆˆ {[i:=x]}, f k y) â‰¡ f i x.
   Proof.
@@ -278,30 +366,37 @@ Section gset.
   Implicit Types X : gset A.
   Implicit Types f : A â†’ M.
 
-  Lemma big_opS_forall R f g X :
+  Lemma big_opS_gen_proper 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.
-    rewrite big_opS_eq. intros ?? Hf. apply (big_opL_forall R); auto.
+    rewrite big_opS_eq. intros ?? Hf. apply (big_opL_gen_proper 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.
+  Proof. apply big_opS_gen_proper; apply _. Qed.
+
+  (** The lemmas [big_opS_ne] and [big_opS_proper] are more generic than the
+  instances as they also give [x âˆˆ X] in the premise. *)
+  Lemma big_opS_ne f g X n :
+    (âˆ€ x, x âˆˆ X â†’ f x â‰¡{n}â‰¡ g x) â†’
+    ([^o set] x âˆˆ X, f x) â‰¡{n}â‰¡ ([^o set] x âˆˆ X, g x).
+  Proof. apply big_opS_gen_proper; 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.
+  Proof. apply big_opS_gen_proper; apply _. Qed.
 
-  Global Instance big_opS_ne n :
+  Global Instance big_opS_ne' n :
     Proper (pointwise_relation _ (dist n) ==> (=) ==> dist n) (big_opS o (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
+  Proof. intros f g Hf m ? <-. apply big_opS_ne; intros; apply Hf. Qed.
   Global Instance big_opS_proper' :
     Proper (pointwise_relation _ (â‰¡) ==> (=) ==> (â‰¡)) (big_opS o (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
+  Proof. intros f g Hf m ? <-. apply big_opS_proper; intros; apply Hf. Qed.
 
   Lemma big_opS_empty f : ([^o set] x âˆˆ âˆ…, f x) = monoid_unit.
   Proof. by rewrite big_opS_eq /big_opS_def elements_empty. Qed.
@@ -365,30 +460,37 @@ Section gmultiset.
   Implicit Types X : gmultiset A.
   Implicit Types f : A â†’ M.
 
-  Lemma big_opMS_forall R f g X :
+  Lemma big_opMS_gen_proper 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.
-    rewrite big_opMS_eq. intros ?? Hf. apply (big_opL_forall R); auto.
+    rewrite big_opMS_eq. intros ?? Hf. apply (big_opL_gen_proper 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.
+  Proof. apply big_opMS_gen_proper; apply _. Qed.
+
+  (** The lemmas [big_opMS_ne] and [big_opMS_proper] are more generic than the
+  instances as they also give [x âˆˆ X] in the premise. *)
+  Lemma big_opMS_ne f g X n :
+    (âˆ€ x, x âˆˆ X â†’ f x â‰¡{n}â‰¡ g x) â†’
+    ([^o mset] x âˆˆ X, f x) â‰¡{n}â‰¡ ([^o mset] x âˆˆ X, g x).
+  Proof. apply big_opMS_gen_proper; 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.
+  Proof. apply big_opMS_gen_proper; apply _. Qed.
 
-  Global Instance big_opMS_ne n :
+  Global Instance big_opMS_ne' n :
     Proper (pointwise_relation _ (dist n) ==> (=) ==> dist n) (big_opMS o (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
+  Proof. intros f g Hf m ? <-. apply big_opMS_ne; intros; apply Hf. Qed.
   Global Instance big_opMS_proper' :
     Proper (pointwise_relation _ (â‰¡) ==> (=) ==> (â‰¡)) (big_opMS o (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
+  Proof. intros f g Hf m ? <-. apply big_opMS_proper; intros; apply Hf. Qed.
 
   Lemma big_opMS_empty f : ([^o mset] x âˆˆ âˆ…, f x) = monoid_unit.
   Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 25bc95c5b11171ea68209a004f7a8a9fa8cab7d2..d499dfa7db0c15fe543000009094b351e4ecf2fb 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -44,32 +44,28 @@ Proof. intros ? m m' ? i. by apply (discrete _). Qed.
 Global Instance gmapO_leibniz: LeibnizEquiv A â†’ LeibnizEquiv gmapO.
 Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
 
-Global Instance lookup_ne k :
-  NonExpansive (lookup k : gmap K A â†’ option A).
+Global Instance lookup_ne k : NonExpansive (lookup k : gmap K A â†’ option A).
 Proof. by intros m1 m2. Qed.
-Global Instance lookup_proper k :
-  Proper ((â‰¡) ==> (â‰¡)) (lookup k : gmap K A â†’ option A) := _.
-Global Instance alter_ne (f : A â†’ A) (k : K) n :
-  Proper (dist n ==> dist n) f â†’ Proper (dist n ==> dist n) (alter f k).
+Global Instance partial_alter_ne n :
+  Proper ((dist n ==> dist n) ==> (=) ==> dist n ==> dist n)
+         (partial_alter (M:=gmap K A)).
 Proof.
-  intros ? m m' Hm k'.
-  by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
-Qed.
-Global Instance insert_ne i :
-  NonExpansive2 (insert (M:=gmap K A) i).
-Proof.
-  intros n x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
-    [by constructor|by apply lookup_ne].
+  by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
+    rewrite ?lookup_partial_alter ?lookup_partial_alter_ne //;
+    try apply Hf; apply lookup_ne.
 Qed.
-Global Instance singleton_ne i :
-  NonExpansive (singletonM i : A â†’ gmap K A).
+Global Instance insert_ne i : NonExpansive2 (insert (M:=gmap K A) i).
+Proof. intros n x y ? m m' ? j; apply partial_alter_ne; by try constructor. Qed.
+Global Instance singleton_ne i : NonExpansive (singletonM i : A â†’ gmap K A).
 Proof. by intros ????; apply insert_ne. Qed.
-Global Instance delete_ne i :
-  NonExpansive (delete (M:=gmap K A) i).
+Global Instance delete_ne i : NonExpansive (delete (M:=gmap K A) i).
 Proof.
   intros n m m' ? j; destruct (decide (i = j)); simplify_map_eq;
     [by constructor|by apply lookup_ne].
 Qed.
+Global Instance alter_ne (f : A â†’ A) (k : K) n :
+  Proper (dist n ==> dist n) f â†’ Proper (dist n ==> dist n) (alter f k).
+Proof. intros ? m m' Hm k'. by apply partial_alter_ne; [solve_proper|..]. Qed.
 
 Global Instance gmap_empty_discrete : Discrete (âˆ… : gmap K A).
 Proof.
@@ -99,6 +95,63 @@ End cofe.
 
 Arguments gmapO _ {_ _} _.
 
+(** Non-expansiveness of higher-order map functions and big-ops *)
+Lemma merge_ne `{Countable K} {A B C : ofeT} (f g : option A â†’ option B â†’ option C)
+    `{!DiagNone f, !DiagNone g} n :
+  ((dist n) ==> (dist n) ==> (dist n))%signature f g â†’
+  ((dist n) ==> (dist n) ==> (dist n))%signature (merge (M:=gmap K) f) (merge g).
+Proof. by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge //; apply Hf. Qed.
+Instance union_with_proper `{Countable K} {A : ofeT} n :
+  Proper (((dist n) ==> (dist n) ==> (dist n)) ==>
+          (dist n) ==> (dist n) ==>(dist n)) (union_with (M:=gmap K A)).
+Proof.
+  intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
+  by do 2 destruct 1; first [apply Hf | constructor].
+Qed.
+Instance map_fmap_proper `{Countable K} {A B : ofeT} (f : A â†’ B) n :
+  Proper (dist n ==> dist n) f â†’ Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
+Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
+Instance map_zip_with_proper `{Countable K} {A B C : ofeT} (f : A â†’ B â†’ C) n :
+  Proper (dist n ==> dist n ==> dist n) f â†’
+  Proper (dist n ==> dist n ==> dist n) (map_zip_with (M:=gmap K) f).
+Proof.
+  intros Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ne; try done.
+  destruct 1; destruct 1; repeat f_equiv; constructor || done.
+Qed.
+
+Lemma big_opM_ne_2 `{Monoid M o} `{Countable K} {A : ofeT} (f g : K â†’ A â†’ M) m1 m2 n :
+  m1 â‰¡{n}â‰¡ m2 â†’
+  (âˆ€ k y1 y2,
+    m1 !! k = Some y1 â†’ m2 !! k = Some y2 â†’ y1 â‰¡{n}â‰¡ y2 â†’ f k y1 â‰¡{n}â‰¡ g k y2) â†’
+  ([^o map] k â†¦ y âˆˆ m1, f k y) â‰¡{n}â‰¡ ([^o map] k â†¦ y âˆˆ m2, g k y).
+Proof.
+  intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
+  { by intros ?? ->. }
+  { apply monoid_ne. }
+  intros k. assert (m1 !! k â‰¡{n}â‰¡ m2 !! k) as Hlk by (by f_equiv).
+  destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
+Qed.
+
+Lemma big_sepM2_ne_2 {PROP : bi} `{Countable K} (A B : ofeT)
+    (Î¦ Î¨ : K â†’ A â†’ B â†’ PROP) m1 m2 m1' m2' n :
+  m1 â‰¡{n}â‰¡ m1' â†’ m2 â‰¡{n}â‰¡ m2' â†’
+  (âˆ€ k y1 y1' y2 y2',
+    m1 !! k = Some y1 â†’ m1' !! k = Some y1' â†’ y1 â‰¡{n}â‰¡ y1' â†’
+    m2 !! k = Some y2 â†’ m2' !! k = Some y2' â†’ y2 â‰¡{n}â‰¡ y2' â†’
+    Î¦ k y1 y2 â‰¡{n}â‰¡ Î¨ k y1' y2') â†’
+  ([âˆ— map] k â†¦ y1;y2 âˆˆ m1;m2, Î¦ k y1 y2)%I â‰¡{n}â‰¡ ([âˆ— map] k â†¦ y1;y2 âˆˆ m1';m2', Î¨ k y1 y2)%I.
+Proof.
+  intros Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
+  { f_equiv; split; intros Hm k.
+    - trans (is_Some (m1 !! k)); [symmetry; apply: is_Some_ne; by f_equiv|].
+      rewrite Hm. apply: is_Some_ne; by f_equiv.
+    - trans (is_Some (m1' !! k)); [apply: is_Some_ne; by f_equiv|].
+      rewrite Hm. symmetry. apply: is_Some_ne; by f_equiv. }
+  apply big_opM_ne_2; [by f_equiv|].
+  intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
+    (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
+Qed.
+
 (* CMRA *)
 Section cmra.
 Context `{Countable K} {A : cmraT}.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 6325e1716d5040c61c7c9c4adca7fc6c32adea7b..669500516482021e9b5cff81e849443ebc3900b2 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -94,13 +94,64 @@ End cofe.
 
 Arguments listO : clear implicits.
 
+(** Non-expansiveness of higher-order list functions and big-ops *)
+Instance list_fmap_ne {A B : ofeT} (f : A â†’ B) n :
+  Proper (dist n ==> dist n) f â†’ Proper (dist n ==> dist n) (fmap (M:=list) f).
+Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
+Instance list_omap_ne {A B : ofeT} (f : A â†’ option B) n :
+  Proper (dist n ==> dist n) f â†’ Proper (dist n ==> dist n) (omap (M:=list) f).
+Proof.
+  intros Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
+  destruct (Hf _ _ Hx); [f_equiv|]; auto.
+Qed.
+Instance imap_ne {A B : ofeT} (f : nat â†’ A â†’ B) n :
+  (âˆ€ i, Proper (dist n ==> dist n) (f i)) â†’ Proper (dist n ==> dist n) (imap f).
+Proof.
+  intros Hf l1 l2 Hl. revert f Hf.
+  induction Hl; intros f Hf; simpl; [constructor|f_equiv; naive_solver].
+Qed.
+Instance list_bind_ne {A B : ofeT} (f : A â†’ list A) n :
+  Proper (dist n ==> dist n) f â†’ Proper (dist n ==> dist n) (mbind f).
+Proof. induction 2; simpl; [constructor|solve_proper]. Qed.
+Instance list_join_ne {A : ofeT} : NonExpansive (mjoin (M:=list) (A:=A)).
+Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
+Instance zip_with_ne {A B C : ofeT} (f : A â†’ B â†’ C) :
+  Proper (dist n ==> dist n ==> dist n) f â†’
+  Proper (dist n ==> dist n ==> dist n) (zip_with f).
+Proof. induction 2; destruct 1; simpl; [constructor..|f_equiv; [f_equiv|]; auto]. Qed.
+
+Lemma big_opL_ne_2 `{Monoid M o} {A : ofeT} (f g : nat â†’ A â†’ M) l1 l2 n :
+  l1 â‰¡{n}â‰¡ l2 â†’
+  (âˆ€ k y1 y2,
+    l1 !! k = Some y1 â†’ l2 !! k = Some y2 â†’ y1 â‰¡{n}â‰¡ y2 â†’ f k y1 â‰¡{n}â‰¡ g k y2) â†’
+  ([^o list] k â†¦ y âˆˆ l1, f k y) â‰¡{n}â‰¡ ([^o list] k â†¦ y âˆˆ l2, g k y).
+Proof.
+  intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
+  { apply monoid_ne. }
+  intros k. assert (l1 !! k â‰¡{n}â‰¡ l2 !! k) as Hlk by (by f_equiv).
+  destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
+Qed.
+
+Lemma big_sepL2_ne_2 {PROP : bi} {A B : ofeT}
+    (Î¦ Î¨ : nat â†’ A â†’ B â†’ PROP) l1 l2 l1' l2' n :
+  l1 â‰¡{n}â‰¡ l1' â†’ l2 â‰¡{n}â‰¡ l2' â†’
+  (âˆ€ k y1 y1' y2 y2',
+    l1 !! k = Some y1 â†’ l1' !! k = Some y1' â†’ y1 â‰¡{n}â‰¡ y1' â†’
+    l2 !! k = Some y2 â†’ l2' !! k = Some y2' â†’ y2 â‰¡{n}â‰¡ y2' â†’
+    Î¦ k y1 y2 â‰¡{n}â‰¡ Î¨ k y1' y2') â†’
+  ([âˆ— list] k â†¦ y1;y2 âˆˆ l1;l2, Î¦ k y1 y2)%I â‰¡{n}â‰¡ ([âˆ— list] k â†¦ y1;y2 âˆˆ l1';l2', Î¨ k y1 y2)%I.
+Proof.
+  intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
+  { do 2 f_equiv; by apply: length_ne. }
+  apply big_opL_ne_2; [by f_equiv|].
+  intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
+    (?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
+Qed.
+
 (** Functor *)
 Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A â†’ B) (l : list A) n :
   (âˆ€ x, f x â‰¡{n}â‰¡ g x) â†’ f <$> l â‰¡{n}â‰¡ g <$> l.
 Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
-Instance list_fmap_ne {A B : ofeT} (f : A â†’ B) n:
-  Proper (dist n ==> dist n) f â†’ Proper (dist n ==> dist n) (fmap (M:=list) f).
-Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
 Definition listO_map {A B} (f : A -n> B) : listO A -n> listO B :=
   OfeMor (fmap f : listO A â†’ listO B).
 Instance listO_map_ne A B : NonExpansive (@listO_map A B).
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 491596e320a6569b84e2462980ec712c5b9a915c..6f57d7fc50db7e479f63ad89efe94a99ccbd6606 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -91,24 +91,33 @@ Section sep_list.
     âŠ£âŠ¢ ([âˆ— list] kâ†¦y âˆˆ l1, Î¦ k y) âˆ— ([âˆ— list] kâ†¦y âˆˆ l2, Î¦ (length l1 + k) y).
   Proof. by rewrite big_opL_app. Qed.
 
+  Lemma big_sepL_submseteq `{BiAffine PROP} (Î¦ : A â†’ PROP) l1 l2 :
+    l1 âŠ†+ l2 â†’ ([âˆ— list] y âˆˆ l2, Î¦ y) âŠ¢ [âˆ— list] y âˆˆ l1, Î¦ y.
+  Proof.
+    intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l.
+  Qed.
+
+  (** The lemmas [big_sepL_mono], [big_sepL_ne] and [big_sepL_proper] are more
+  generic than the instances as they also give [l !! k = Some y] in the premise. *)
   Lemma big_sepL_mono Î¦ Î¨ l :
     (âˆ€ k y, l !! k = Some y â†’ Î¦ k y âŠ¢ Î¨ k y) â†’
     ([âˆ— list] k â†¦ y âˆˆ l, Î¦ k y) âŠ¢ [âˆ— list] k â†¦ y âˆˆ l, Î¨ k y.
-  Proof. apply big_opL_forall; apply _. Qed.
+  Proof. apply big_opL_gen_proper; apply _. Qed.
+  Lemma big_sepL_ne Î¦ Î¨ l n :
+    (âˆ€ k y, l !! k = Some y â†’ Î¦ k y â‰¡{n}â‰¡ Î¨ k y) â†’
+    ([âˆ— list] k â†¦ y âˆˆ l, Î¦ k y)%I â‰¡{n}â‰¡ ([âˆ— list] k â†¦ y âˆˆ l, Î¨ k y)%I.
+  Proof. apply big_opL_ne. Qed.
   Lemma big_sepL_proper Î¦ Î¨ l :
     (âˆ€ k y, l !! k = Some y â†’ Î¦ k y âŠ£âŠ¢ Î¨ k y) â†’
     ([âˆ— list] k â†¦ y âˆˆ l, Î¦ k y) âŠ£âŠ¢ ([âˆ— list] k â†¦ y âˆˆ l, Î¨ k y).
   Proof. apply big_opL_proper. Qed.
-  Lemma big_sepL_submseteq `{BiAffine PROP} (Î¦ : A â†’ PROP) l1 l2 :
-    l1 âŠ†+ l2 â†’ ([âˆ— list] y âˆˆ l2, Î¦ y) âŠ¢ [âˆ— list] y âˆˆ l1, Î¦ y.
-  Proof.
-    intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l.
-  Qed.
 
+  (** No need to declare instances for non-expansiveness and properness, we
+  get both from the generic [big_opL] instances. *)
   Global Instance big_sepL_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (âŠ¢)) ==> (=) ==> (âŠ¢))
            (big_opL (@bi_sep PROP) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
+  Proof. intros f g Hf m ? <-. apply big_sepL_mono; intros; apply Hf. Qed.
   Global Instance big_sepL_id_mono' :
     Proper (Forall2 (âŠ¢) ==> (âŠ¢)) (big_opL (@bi_sep PROP) (Î» _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
@@ -349,6 +358,8 @@ Section sep_list2.
     - by rewrite -assoc IH.
   Qed.
 
+  (** The lemmas [big_sepL2_mono], [big_sepL2_ne] and [big_sepL2_proper] are more
+  generic than the instances as they also give [li !! k = Some yi] in the premise. *)
   Lemma big_sepL2_mono Î¦ Î¨ l1 l2 :
     (âˆ€ k y1 y2, l1 !! k = Some y1 â†’ l2 !! k = Some y2 â†’ Î¦ k y1 y2 âŠ¢ Î¨ k y1 y2) â†’
     ([âˆ— list] k â†¦ y1;y2 âˆˆ l1;l2, Î¦ k y1 y2) âŠ¢ [âˆ— list] k â†¦ y1;y2 âˆˆ l1;l2, Î¨ k y1 y2.
@@ -356,6 +367,13 @@ Section sep_list2.
     intros H. rewrite !big_sepL2_alt. f_equiv. apply big_sepL_mono=> k [y1 y2].
     rewrite lookup_zip_with=> ?; simplify_option_eq; auto.
   Qed.
+  Lemma big_sepL2_ne Î¦ Î¨ l1 l2 n :
+    (âˆ€ k y1 y2, l1 !! k = Some y1 â†’ l2 !! k = Some y2 â†’ Î¦ k y1 y2 â‰¡{n}â‰¡ Î¨ k y1 y2) â†’
+    ([âˆ— list] k â†¦ y1;y2 âˆˆ l1;l2, Î¦ k y1 y2)%I â‰¡{n}â‰¡ ([âˆ— list] k â†¦ y1;y2 âˆˆ l1;l2, Î¨ k y1 y2)%I.
+  Proof.
+    intros H. rewrite !big_sepL2_alt. f_equiv. apply big_sepL_ne=> k [y1 y2].
+    rewrite lookup_zip_with=> ?; simplify_option_eq; auto.
+  Qed.
   Lemma big_sepL2_proper Î¦ Î¨ l1 l2 :
     (âˆ€ k y1 y2, l1 !! k = Some y1 â†’ l2 !! k = Some y2 â†’ Î¦ k y1 y2 âŠ£âŠ¢ Î¨ k y1 y2) â†’
     ([âˆ— list] k â†¦ y1;y2 âˆˆ l1;l2, Î¦ k y1 y2) âŠ£âŠ¢ [âˆ— list] k â†¦ y1;y2 âˆˆ l1;l2, Î¨ k y1 y2.
@@ -363,15 +381,26 @@ Section sep_list2.
     intros; apply (anti_symm _);
       apply big_sepL2_mono; auto using equiv_entails, equiv_entails_sym.
   Qed.
+  Lemma big_sepL2_proper_2 `{!Equiv A, !Equiv B} Î¦ Î¨ l1 l2 l1' l2' :
+    l1 â‰¡ l1' â†’ l2 â‰¡ l2' â†’
+    (âˆ€ k y1 y1' y2 y2',
+      l1 !! k = Some y1 â†’ l1' !! k = Some y1' â†’ y1 â‰¡ y1' â†’
+      l2 !! k = Some y2 â†’ l2' !! k = Some y2' â†’ y2 â‰¡ y2' â†’
+      Î¦ k y1 y2 âŠ£âŠ¢ Î¨ k y1' y2') â†’
+    ([âˆ— list] k â†¦ y1;y2 âˆˆ l1;l2, Î¦ k y1 y2) âŠ£âŠ¢ [âˆ— list] k â†¦ y1;y2 âˆˆ l1';l2', Î¨ k y1 y2.
+  Proof.
+    intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
+    { do 2 f_equiv; by apply length_proper. }
+    apply big_opL_proper_2; [by f_equiv|].
+    intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
+      (?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
+  Qed.
 
-  Global Instance big_sepL2_ne n :
+  Global Instance big_sepL2_ne' n :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (dist n)))
       ==> (=) ==> (=) ==> (dist n))
            (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
-  Proof.
-    intros Î¦1 Î¦2 HÎ¦ x1 ? <- x2 ? <-. rewrite !big_sepL2_alt. f_equiv.
-    f_equiv=> k [y1 y2]. apply HÎ¦.
-  Qed.
+  Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_ne; intros; apply Hf. Qed.
   Global Instance big_sepL2_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (âŠ¢)))
       ==> (=) ==> (=) ==> (âŠ¢))
@@ -499,24 +528,33 @@ Section and_list.
     âŠ£âŠ¢ ([âˆ§ list] kâ†¦y âˆˆ l1, Î¦ k y) âˆ§ ([âˆ§ list] kâ†¦y âˆˆ l2, Î¦ (length l1 + k) y).
   Proof. by rewrite big_opL_app. Qed.
 
+  Lemma big_andL_submseteq (Î¦ : A â†’ PROP) l1 l2 :
+    l1 âŠ†+ l2 â†’ ([âˆ§ list] y âˆˆ l2, Î¦ y) âŠ¢ [âˆ§ list] y âˆˆ l1, Î¦ y.
+  Proof.
+    intros [l ->]%submseteq_Permutation. by rewrite big_andL_app and_elim_l.
+  Qed.
+
+  (** The lemmas [big_andL_mono], [big_andL_ne] and [big_andL_proper] are more
+  generic than the instances as they also give [l !! k = Some y] in the premise. *)
   Lemma big_andL_mono Î¦ Î¨ l :
     (âˆ€ k y, l !! k = Some y â†’ Î¦ k y âŠ¢ Î¨ k y) â†’
     ([âˆ§ list] k â†¦ y âˆˆ l, Î¦ k y) âŠ¢ [âˆ§ list] k â†¦ y âˆˆ l, Î¨ k y.
-  Proof. apply big_opL_forall; apply _. Qed.
+  Proof. apply big_opL_gen_proper; apply _. Qed.
+  Lemma big_andL_ne Î¦ Î¨ l n :
+    (âˆ€ k y, l !! k = Some y â†’ Î¦ k y â‰¡{n}â‰¡ Î¨ k y) â†’
+    ([âˆ§ list] k â†¦ y âˆˆ l, Î¦ k y)%I â‰¡{n}â‰¡ ([âˆ§ list] k â†¦ y âˆˆ l, Î¨ k y)%I.
+  Proof. apply big_opL_ne. Qed.
   Lemma big_andL_proper Î¦ Î¨ l :
     (âˆ€ k y, l !! k = Some y â†’ Î¦ k y âŠ£âŠ¢ Î¨ k y) â†’
     ([âˆ§ list] k â†¦ y âˆˆ l, Î¦ k y) âŠ£âŠ¢ ([âˆ§ list] k â†¦ y âˆˆ l, Î¨ k y).
   Proof. apply big_opL_proper. Qed.
-  Lemma big_andL_submseteq (Î¦ : A â†’ PROP) l1 l2 :
-    l1 âŠ†+ l2 â†’ ([âˆ§ list] y âˆˆ l2, Î¦ y) âŠ¢ [âˆ§ list] y âˆˆ l1, Î¦ y.
-  Proof.
-    intros [l ->]%submseteq_Permutation. by rewrite big_andL_app and_elim_l.
-  Qed.
 
+  (** No need to declare instances for non-expansiveness and properness, we
+  get both from the generic [big_opL] instances. *)
   Global Instance big_andL_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (âŠ¢)) ==> (=) ==> (âŠ¢))
            (big_opL (@bi_and PROP) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
+  Proof. intros f g Hf m ? <-. apply big_andL_mono; intros; apply Hf. Qed.
   Global Instance big_andL_id_mono' :
     Proper (Forall2 (âŠ¢) ==> (âŠ¢)) (big_opL (@bi_and PROP) (Î» _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
@@ -589,24 +627,33 @@ Section or_list.
     âŠ£âŠ¢ ([âˆ¨ list] kâ†¦y âˆˆ l1, Î¦ k y) âˆ¨ ([âˆ¨ list] kâ†¦y âˆˆ l2, Î¦ (length l1 + k) y).
   Proof. by rewrite big_opL_app. Qed.
 
+  Lemma big_orL_submseteq (Î¦ : A â†’ PROP) l1 l2 :
+    l1 âŠ†+ l2 â†’ ([âˆ¨ list] y âˆˆ l1, Î¦ y) âŠ¢ [âˆ¨ list] y âˆˆ l2, Î¦ y.
+  Proof.
+    intros [l ->]%submseteq_Permutation. by rewrite big_orL_app -or_intro_l.
+  Qed.
+
+  (** The lemmas [big_orL_mono], [big_orL_ne] and [big_orL_proper] are more
+  generic than the instances as they also give [l !! k = Some y] in the premise. *)
   Lemma big_orL_mono Î¦ Î¨ l :
     (âˆ€ k y, l !! k = Some y â†’ Î¦ k y âŠ¢ Î¨ k y) â†’
     ([âˆ¨ list] k â†¦ y âˆˆ l, Î¦ k y) âŠ¢ [âˆ¨ list] k â†¦ y âˆˆ l, Î¨ k y.
-  Proof. apply big_opL_forall; apply _. Qed.
+  Proof. apply big_opL_gen_proper; apply _. Qed.
+  Lemma big_orL_ne Î¦ Î¨ l n :
+    (âˆ€ k y, l !! k = Some y â†’ Î¦ k y â‰¡{n}â‰¡ Î¨ k y) â†’
+    ([âˆ¨ list] k â†¦ y âˆˆ l, Î¦ k y)%I â‰¡{n}â‰¡ ([âˆ¨ list] k â†¦ y âˆˆ l, Î¨ k y)%I.
+  Proof. apply big_opL_ne. Qed.
   Lemma big_orL_proper Î¦ Î¨ l :
     (âˆ€ k y, l !! k = Some y â†’ Î¦ k y âŠ£âŠ¢ Î¨ k y) â†’
     ([âˆ¨ list] k â†¦ y âˆˆ l, Î¦ k y) âŠ£âŠ¢ ([âˆ¨ list] k â†¦ y âˆˆ l, Î¨ k y).
   Proof. apply big_opL_proper. Qed.
-  Lemma big_orL_submseteq (Î¦ : A â†’ PROP) l1 l2 :
-    l1 âŠ†+ l2 â†’ ([âˆ¨ list] y âˆˆ l1, Î¦ y) âŠ¢ [âˆ¨ list] y âˆˆ l2, Î¦ y.
-  Proof.
-    intros [l ->]%submseteq_Permutation. by rewrite big_orL_app -or_intro_l.
-  Qed.
 
+  (** No need to declare instances for non-expansiveness and properness, we
+  get both from the generic [big_opL] instances. *)
   Global Instance big_orL_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (âŠ¢)) ==> (=) ==> (âŠ¢))
            (big_opL (@bi_or PROP) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
+  Proof. intros f g Hf m ? <-. apply big_orL_mono; intros; apply Hf. Qed.
   Global Instance big_orL_id_mono' :
     Proper (Forall2 (âŠ¢) ==> (âŠ¢)) (big_opL (@bi_or PROP) (Î» _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
@@ -680,22 +727,31 @@ Section map.
   Implicit Types m : gmap K A.
   Implicit Types Î¦ Î¨ : K â†’ A â†’ PROP.
 
+  Lemma big_sepM_subseteq `{BiAffine PROP} Î¦ m1 m2 :
+    m2 âŠ† m1 â†’ ([âˆ— map] k â†¦ x âˆˆ m1, Î¦ k x) âŠ¢ [âˆ— map] k â†¦ x âˆˆ m2, Î¦ k x.
+  Proof. rewrite big_opM_eq. intros. by apply big_sepL_submseteq, map_to_list_submseteq. Qed.
+
+  (** The lemmas [big_sepM_mono], [big_sepM_ne] and [big_sepM_proper] are more
+  generic than the instances as they also give [l !! k = Some y] in the premise. *)
   Lemma big_sepM_mono Î¦ Î¨ m :
     (âˆ€ k x, m !! k = Some x â†’ Î¦ k x âŠ¢ Î¨ k x) â†’
     ([âˆ— map] k â†¦ x âˆˆ m, Î¦ k x) âŠ¢ [âˆ— map] k â†¦ x âˆˆ m, Î¨ k x.
-  Proof. apply big_opM_forall; apply _ || auto. Qed.
+  Proof. apply big_opM_gen_proper; apply _ || auto. Qed.
+  Lemma big_sepM_ne Î¦ Î¨ m n :
+    (âˆ€ k x, m !! k = Some x â†’ Î¦ k x â‰¡{n}â‰¡ Î¨ k x) â†’
+    ([âˆ— map] k â†¦ x âˆˆ m, Î¦ k x)%I â‰¡{n}â‰¡ ([âˆ— map] k â†¦ x âˆˆ m, Î¨ k x)%I.
+  Proof. apply big_opM_ne. Qed.
   Lemma big_sepM_proper Î¦ Î¨ m :
     (âˆ€ k x, m !! k = Some x â†’ Î¦ k x âŠ£âŠ¢ Î¨ k x) â†’
     ([âˆ— map] k â†¦ x âˆˆ m, Î¦ k x) âŠ£âŠ¢ ([âˆ— map] k â†¦ x âˆˆ m, Î¨ k x).
   Proof. apply big_opM_proper. Qed.
-  Lemma big_sepM_subseteq `{BiAffine PROP} Î¦ m1 m2 :
-    m2 âŠ† m1 â†’ ([âˆ— map] k â†¦ x âˆˆ m1, Î¦ k x) âŠ¢ [âˆ— map] k â†¦ x âˆˆ m2, Î¦ k x.
-  Proof. rewrite big_opM_eq. intros. by apply big_sepL_submseteq, map_to_list_submseteq. Qed.
 
+  (** No need to declare instances for non-expansiveness and properness, we
+  get both from the generic [big_opM] instances. *)
   Global Instance big_sepM_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (âŠ¢)) ==> (=) ==> (âŠ¢))
            (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
-  Proof. intros f g Hf m ? <-. apply big_sepM_mono=> ???; apply Hf. Qed.
+  Proof. intros f g Hf m ? <-. apply big_sepM_mono; intros; apply Hf. Qed.
 
   Lemma big_sepM_empty Î¦ : ([âˆ— map] kâ†¦x âˆˆ âˆ…, Î¦ k x) âŠ£âŠ¢ emp.
   Proof. by rewrite big_opM_empty. Qed.
@@ -876,6 +932,8 @@ Section map2.
     set_unfold=>k. by rewrite !elem_of_dom.
   Qed.
 
+  (** The lemmas [big_sepM2_mono], [big_sepM2_ne] and [big_sepM2_proper] are more
+  generic than the instances as they also give [mi !! k = Some yi] in the premise. *)
   Lemma big_sepM2_mono Î¦ Î¨ m1 m2 :
     (âˆ€ k y1 y2, m1 !! k = Some y1 â†’ m2 !! k = Some y2 â†’ Î¦ k y1 y2 âŠ¢ Î¨ k y1 y2) â†’
     ([âˆ— map] k â†¦ y1;y2 âˆˆ m1;m2, Î¦ k y1 y2) âŠ¢ [âˆ— map] k â†¦ y1;y2 âˆˆ m1;m2, Î¨ k y1 y2.
@@ -888,6 +946,17 @@ Section map2.
     destruct (m2 !! k) as [y2|]; simpl; last done.
     intros ?; simplify_eq. by apply Hm1m2.
   Qed.
+  Lemma big_sepM2_ne Î¦ Î¨ m1 m2 n :
+    (âˆ€ k y1 y2, m1 !! k = Some y1 â†’ m2 !! k = Some y2 â†’ Î¦ k y1 y2 â‰¡{n}â‰¡ Î¨ k y1 y2) â†’
+    ([âˆ— map] k â†¦ y1;y2 âˆˆ m1;m2, Î¦ k y1 y2)%I â‰¡{n}â‰¡ ([âˆ— map] k â†¦ y1;y2 âˆˆ m1;m2, Î¨ k y1 y2)%I.
+  Proof.
+    intros Hm1m2. rewrite big_sepM2_eq /big_sepM2_def.
+    f_equiv. apply big_sepM_ne=> k [x1 x2]. rewrite map_lookup_zip_with.
+    specialize (Hm1m2 k x1 x2).
+    destruct (m1 !! k) as [y1|]; last done.
+    destruct (m2 !! k) as [y2|]; simpl; last done.
+    intros ?; simplify_eq. by apply Hm1m2.
+  Qed.
   Lemma big_sepM2_proper Î¦ Î¨ m1 m2 :
     (âˆ€ k y1 y2, m1 !! k = Some y1 â†’ m2 !! k = Some y2 â†’ Î¦ k y1 y2 âŠ£âŠ¢ Î¨ k y1 y2) â†’
     ([âˆ— map] k â†¦ y1;y2 âˆˆ m1;m2, Î¦ k y1 y2) âŠ£âŠ¢ [âˆ— map] k â†¦ y1;y2 âˆˆ m1;m2, Î¨ k y1 y2.
@@ -895,15 +964,30 @@ Section map2.
     intros; apply (anti_symm _);
       apply big_sepM2_mono; auto using equiv_entails, equiv_entails_sym.
   Qed.
-
-  Global Instance big_sepM2_ne n :
+  Lemma big_sepM2_proper_2 `{!Equiv A, !Equiv B} Î¦ Î¨ m1 m2 m1' m2' :
+    m1 â‰¡ m1' â†’ m2 â‰¡ m2' â†’
+    (âˆ€ k y1 y1' y2 y2',
+      m1 !! k = Some y1 â†’ m1' !! k = Some y1' â†’ y1 â‰¡ y1' â†’
+      m2 !! k = Some y2 â†’ m2' !! k = Some y2' â†’ y2 â‰¡ y2' â†’
+      Î¦ k y1 y2 âŠ£âŠ¢ Î¨ k y1' y2') â†’
+    ([âˆ— map] k â†¦ y1;y2 âˆˆ m1;m2, Î¦ k y1 y2) âŠ£âŠ¢ [âˆ— map] k â†¦ y1;y2 âˆˆ m1';m2', Î¨ k y1 y2.
+  Proof.
+    intros Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
+    { f_equiv; split; intros Hm k.
+      - trans (is_Some (m1 !! k)); [symmetry; apply is_Some_proper; by f_equiv|].
+        rewrite Hm. apply is_Some_proper; by f_equiv.
+      - trans (is_Some (m1' !! k)); [apply is_Some_proper; by f_equiv|].
+        rewrite Hm. symmetry. apply is_Some_proper; by f_equiv. }
+    apply big_opM_proper_2; [by f_equiv|].
+    intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
+      (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
+  Qed.
+
+  Global Instance big_sepM2_ne' n :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (dist n)))
       ==> (=) ==> (=) ==> (dist n))
            (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
-  Proof.
-    intros Î¦1 Î¦2 HÎ¦ x1 ? <- x2 ? <-. rewrite big_sepM2_eq /big_sepM2_def.
-    f_equiv. f_equiv=> k [y1 y2]. apply HÎ¦.
-  Qed.
+  Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_ne; intros; apply Hf. Qed.
   Global Instance big_sepM2_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (âŠ¢)))
       ==> (=) ==> (=) ==> (âŠ¢)) (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
@@ -1182,18 +1266,27 @@ Section gset.
   Implicit Types X : gset A.
   Implicit Types Î¦ : A â†’ PROP.
 
+  Lemma big_sepS_subseteq `{BiAffine PROP} Î¦ X Y :
+    Y âŠ† X â†’ ([âˆ— set] x âˆˆ X, Î¦ x) âŠ¢ [âˆ— set] x âˆˆ Y, Î¦ x.
+  Proof. rewrite big_opS_eq. intros. by apply big_sepL_submseteq, elements_submseteq. Qed.
+
+  (** The lemmas [big_sepS_mono], [big_sepS_ne] and [big_sepS_proper] are more
+  generic than the instances as they also give [x âˆˆ X] in the premise. *)
   Lemma big_sepS_mono Î¦ Î¨ X :
     (âˆ€ x, x âˆˆ X â†’ Î¦ x âŠ¢ Î¨ x) â†’
     ([âˆ— set] x âˆˆ X, Î¦ x) âŠ¢ [âˆ— set] x âˆˆ X, Î¨ x.
-  Proof. intros. apply big_opS_forall; apply _ || auto. Qed.
+  Proof. intros. apply big_opS_gen_proper; apply _ || auto. Qed.
+  Lemma big_sepS_ne Î¦ Î¨ X n :
+    (âˆ€ x, x âˆˆ X â†’ Î¦ x â‰¡{n}â‰¡ Î¨ x) â†’
+    ([âˆ— set] x âˆˆ X, Î¦ x)%I â‰¡{n}â‰¡ ([âˆ— set] x âˆˆ X, Î¨ x)%I.
+  Proof. apply big_opS_ne. 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.
-  Lemma big_sepS_subseteq `{BiAffine PROP} Î¦ X Y :
-    Y âŠ† X â†’ ([âˆ— set] x âˆˆ X, Î¦ x) âŠ¢ [âˆ— set] x âˆˆ Y, Î¦ x.
-  Proof. rewrite big_opS_eq. intros. by apply big_sepL_submseteq, elements_submseteq. Qed.
 
+  (** No need to declare instances for non-expansiveness and properness, we
+  get both from the generic [big_opS] instances. *)
   Global Instance big_sepS_mono' :
      Proper (pointwise_relation _ (âŠ¢) ==> (=) ==> (âŠ¢)) (big_opS (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed.
@@ -1344,18 +1437,27 @@ Section gmultiset.
   Implicit Types X : gmultiset A.
   Implicit Types Î¦ : A â†’ PROP.
 
+  Lemma big_sepMS_subseteq `{BiAffine PROP} Î¦ X Y :
+    Y âŠ† X â†’ ([âˆ— mset] x âˆˆ X, Î¦ x) âŠ¢ [âˆ— mset] x âˆˆ Y, Î¦ x.
+  Proof. rewrite big_opMS_eq. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed.
+
+  (** The lemmas [big_sepMS_mono], [big_sepMS_ne] and [big_sepMS_proper] are more
+  generic than the instances as they also give [l !! k = Some y] in the premise. *)
   Lemma big_sepMS_mono Î¦ Î¨ X :
     (âˆ€ x, x âˆˆ X â†’ Î¦ x âŠ¢ Î¨ x) â†’
     ([âˆ— mset] x âˆˆ X, Î¦ x) âŠ¢ [âˆ— mset] x âˆˆ X, Î¨ x.
-  Proof. intros. apply big_opMS_forall; apply _ || auto. Qed.
+  Proof. intros. apply big_opMS_gen_proper; apply _ || auto. Qed.
+  Lemma big_sepMS_ne Î¦ Î¨ X n :
+    (âˆ€ x, x âˆˆ X â†’ Î¦ x â‰¡{n}â‰¡ Î¨ x) â†’
+    ([âˆ— mset] x âˆˆ X, Î¦ x)%I â‰¡{n}â‰¡ ([âˆ— mset] x âˆˆ X, Î¨ x)%I.
+  Proof. apply big_opMS_ne. 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.
-  Lemma big_sepMS_subseteq `{BiAffine PROP} Î¦ X Y :
-    Y âŠ† X â†’ ([âˆ— mset] x âˆˆ X, Î¦ x) âŠ¢ [âˆ— mset] x âˆˆ Y, Î¦ x.
-  Proof. rewrite big_opMS_eq. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed.
 
+  (** No need to declare instances for non-expansiveness and properness, we
+  get both from the generic [big_opMS] instances. *)
   Global Instance big_sepMS_mono' :
      Proper (pointwise_relation _ (âŠ¢) ==> (=) ==> (âŠ¢)) (big_opMS (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. by apply big_sepMS_mono. Qed.