Commit 4a1eb8a3 authored by Robbert Krebbers's avatar Robbert Krebbers

Property about bigops and replicate.

parent df0bf3ac
...@@ -186,6 +186,10 @@ Section sep_list. ...@@ -186,6 +186,10 @@ Section sep_list.
rewrite -decide_emp. by repeat case_decide. rewrite -decide_emp. by repeat case_decide.
Qed. 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 Φ : Global Instance big_sepL_nil_persistent Φ :
Persistent ([ list] kx [], Φ k x). Persistent ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed. Proof. simpl; apply _. Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment