diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 98b92bab8bbdf9851b43ba7755e659cd2a6c90ca..dd9e84b1c421a7d3aebc6963f736d2e8eab35076 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -186,6 +186,10 @@ Section sep_list.
     rewrite -decide_emp. by repeat case_decide.
   Qed.
 
+  Lemma big_sepL_replicate l P :
+    [∗] replicate (length l) P ⊣⊢ [∗ list] y ∈ l, P.
+  Proof. induction l as [|x l]=> //=; by f_equiv. Qed.
+
   Global Instance big_sepL_nil_persistent Φ :
     Persistent ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.