From 4b47dc0b135f0631645fb73d42348e397d69931a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 25 Jun 2021 09:11:47 +0200
Subject: [PATCH] add big_sepS_delete_2

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

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 60a087b43..71d2496bc 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2090,6 +2090,14 @@ Section gset.
   Lemma big_sepS_delete Φ X x :
     x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y.
   Proof. apply big_opS_delete. Qed.
+  Lemma big_sepS_delete_2 `{!BiAffine PROP} Φ X x :
+    Φ x ∗ ([∗ set] y ∈ X ∖ {[ x ]}, Φ y) ⊢ [∗ set] y ∈ X, Φ y.
+  Proof.
+    destruct (decide (x ∈ X)).
+    - rewrite -big_sepS_delete //.
+    - replace (X ∖ {[x]}) with X by set_solver.
+      rewrite bi.sep_elim_r. done.
+  Qed.
 
   Lemma big_sepS_elem_of Φ X x `{!Absorbing (Φ x)} :
     x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x.
-- 
GitLab