diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 42f06e44bb200f124bb90628c036c7b2f093ea75..5c34694b7c4a965b52317fb5744a698ddfbca5e8 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -157,6 +157,9 @@ Section list.
   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_contains (f : A → M) l1 l2 :
+    l1 `contains` l2 → ([⋅ list] x ∈ l1, f x) ≼ ([⋅ list] x ∈ l2, f x).
+  Proof. intros Hl. apply big_op_contains. rewrite !imap_const. by rewrite ->Hl. Qed.
 
   Global Instance big_opL_ne l n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index 088389bb374bf30a11085b80e080827276dd69b6..17df7d6928d8d1eeb50ac51ce0a435cb196fb081 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -219,6 +219,9 @@ Section list.
     (∀ 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_contains (Φ : A → uPred M) l1 l2 :
+    l1 `contains` l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
+  Proof. intros ?. apply uPred_included. by apply: big_opL_contains. Qed.
 
   Global Instance big_sepL_mono' l :
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))