diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index ce7886b0101bbc392aca224563ceb35d583a370b..8a4160431f6788b3b6393aa226f060d18b6f5590 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -154,6 +154,13 @@ Section list.
     (∀ 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.
+    assert (∀ l, imap (λ _ x, f x) l = map f l) as EQ;
+      last by rewrite /big_opL !EQ=>->.
+    intros l; revert f. induction l as [|?? IH]=>// f. rewrite imap_cons IH //.
+  Qed.
 
   Global Instance big_opL_ne l n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))