diff --git a/iris/algebra/gset.v b/iris/algebra/gset.v
index 709d8f28974c46cde25a7cab6bdac7b09dadc45a..f72c6ab8b396ac70f7a306586d0801b935d71ee4 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,