From 4a1eb8a3d20789af6265b9011939be8274da042c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 31 Oct 2018 17:16:43 +0100
Subject: [PATCH] Property about bigops and replicate.

---
 theories/bi/big_op.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 98b92bab8..dd9e84b1c 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.
-- 
GitLab