Commit 5cbe3c8e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Prove [fupd_big_sepL].

parent 87abb52a
......@@ -121,6 +121,12 @@ Qed.
Lemma fupd_sep E P Q : (|={E}=> P) (|={E}=> Q) ={E}= P Q.
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
Lemma fupd_big_sepL {A} E (Φ : nat A iProp Σ) (l : list A) :
([ list] kx l, |={E}=> Φ k x) ={E}= [ list] kx l, Φ k x.
Proof.
apply (big_opL_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K A iProp Σ) (m : gmap K A) :
([ map] kx m, |={E}=> Φ k x) ={E}= [ map] kx m, Φ k x.
Proof.
......
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