From 50d5afedefd7ba7b209152591bd2b91004216790 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 25 Jun 2021 09:14:05 +0200
Subject: [PATCH] add big_sepS_insert_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 71d2496bc..007fc5e96 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2071,6 +2071,14 @@ Section gset.
   Lemma big_sepS_insert Φ X x :
     x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ∗ [∗ set] y ∈ X, Φ y).
   Proof. apply big_opS_insert. Qed.
+  Lemma big_sepS_insert_2 `{!BiAffine PROP} Φ X x :
+    (Φ x ∗ [∗ set] y ∈ X, Φ y) ⊢ ([∗ set] y ∈ {[ x ]} ∪ X, Φ y).
+  Proof.
+    destruct (decide (x ∈ X)).
+    - rewrite bi.sep_elim_r. replace ({[x]} ∪ X) with X by set_solver.
+      done.
+    - rewrite -big_sepS_insert //.
+  Qed.
 
   Lemma big_sepS_fn_insert {B} (Ψ : A → B → PROP) f X x b :
     x ∉ X →
-- 
GitLab