From d6139cd3d1443d26f8860d229ba210b93d15f246 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 May 2021 12:26:22 +0200
Subject: [PATCH] strengthen big_sepS_sepS to bi-entailment

---
 iris/bi/big_op.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 6209dbf57..5bc3420c0 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2251,7 +2251,7 @@ End gset.
 
 Lemma big_sepS_sepS `{Countable A, Countable B}
     (X : gset A) (Y : gset B) (Φ : A → B → PROP) :
-  ([∗ set] x ∈ X, [∗ set] y ∈ Y, Φ x y) -∗ ([∗ set] y ∈ Y, [∗ set] x ∈ X, Φ x y).
+  ([∗ set] x ∈ X, [∗ set] y ∈ Y, Φ x y) ⊣⊢ ([∗ set] y ∈ Y, [∗ set] x ∈ X, Φ x y).
 Proof.
   repeat setoid_rewrite big_sepS_elements.
   rewrite big_sepL_sepL. done.
-- 
GitLab