From ebd33ba012ebeb19037ca72a27eb87a38951d47f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 Nov 2022 17:17:20 +0100
Subject: [PATCH] add GSet_inj

---
 iris/algebra/gset.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/iris/algebra/gset.v b/iris/algebra/gset.v
index 709d8f289..f72c6ab8b 100644
--- a/iris/algebra/gset.v
+++ b/iris/algebra/gset.v
@@ -83,6 +83,9 @@ Section gset_disj.
   Local Arguments cmra_op _ !_ !_ /.
   Local Arguments ucmra_op _ !_ !_ /.
 
+  Global Instance GSet_inj : Inj (=@{gset K}) (=) GSet.
+  Proof. intros ???. naive_solver. Qed.
+
   Canonical Structure gset_disjO := leibnizO (gset_disj K).
 
   Local Instance gset_disj_valid_instance : Valid (gset_disj K) := λ X,
-- 
GitLab