diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index a2c6dd5da2b0227b90d66a3fcdd0bb1497c6a756..65f9f9256d7c8a4407c5d438ae768a685aff804f 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra list.
 From iris.prelude Require Import gmap.
 
 Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
@@ -25,8 +25,9 @@ Proof.
   - by rewrite !assoc (comm _ x).
   - by trans (big_op xs2).
 Qed.
-Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
+Global Instance big_op_ne n : Proper (dist n ==> dist n) big_op.
 Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
+Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op := ne_proper _.
 Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
 Proof.
   induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index f7fd01d7d415bb539e0d794a3624a86616d6ae31..fe35a51e6d93ee631b01471bdbac8abac5129aff 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export upred.
+From iris.algebra Require Export upred list.
 From iris.prelude Require Import gmap fin_collections.
 Import uPred.
 
@@ -44,11 +44,9 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 Global Instance big_sep_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_sep M).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
-Global Instance big_and_ne n :
-  Proper (Forall2 (dist n) ==> dist n) (@uPred_big_and M).
+Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_sep_ne n :
-  Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M).
+Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
 Global Instance big_and_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_and M).