From f56f3834362bd1fc6d42ece137114ccd61043a0a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Nov 2020 22:05:56 +0100
Subject: [PATCH] add big_sepS_elem_of_acc_impl

---
 iris/bi/big_op.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 44a785eec..11a71136e 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1782,6 +1782,22 @@ Section gset.
     by setoid_rewrite wand_elim_l.
   Qed.
 
+  Lemma big_sepS_elem_of_acc_impl x Φ X :
+    x ∈ X →
+    ([∗ set] y ∈ X, Φ y) -∗ Φ x ∗
+      (∀ Ψ, Ψ x -∗ □ (∀ y, ⌜y ∈ X ∧ y ≠ x⌝ → Φ y -∗ Ψ y) -∗ ([∗ set] y ∈ X, Ψ y)).
+  Proof.
+    intros Helem. rewrite big_sepS_delete //. apply sep_mono_r.
+    apply forall_intro=>Ψ.
+    rewrite (big_sepS_impl Φ Ψ).
+    rewrite wand_curry comm -wand_curry. apply wand_intro_r.
+    assert (∀ a : A, a ∈ X ∧ a ≠ x ↔ a ∈ X ∖ {[x]}) as Hiff by set_solver.
+    setoid_rewrite Hiff.
+    rewrite wand_elim_l.
+    apply wand_intro_l.
+    rewrite -big_sepS_delete //.
+  Qed.
+
   Lemma big_sepS_dup P `{!Affine P} X :
     □ (P -∗ P ∗ P) -∗ P -∗ [∗ set] x ∈ X, P.
   Proof.
-- 
GitLab