add big_sepS_elem_of_acc_impl

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.