From f2098383dd6fe9c60010cbc73ec820cea6c38768 Mon Sep 17 00:00:00 2001
From: Marijn van Wezel <marijn@wikibase.nl>
Date: Thu, 17 Oct 2024 15:40:11 +0200
Subject: [PATCH] Rewrite injectivity lemma to instance of Inj

---
 stdpp/gmultiset.v | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index b72865c8..6cf5d940 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -821,15 +821,13 @@ Section map.
     - rewrite gmultiset_map_disj_union, gmultiset_map_singleton, !multiplicity_disj_union.
       destruct (bool_decide (x = x')); multiset_solver.
   Qed.
-
-  Lemma gmultiset_map_eq_iff f X Y :
-    Inj (=) (=) f → gmultiset_map f X = gmultiset_map f Y ↔ X = Y.
+  
+  Global Instance gmultiset_map_inj f : Inj (=) (=) f → Inj (=) (=) (gmultiset_map f).
   Proof.
-    intros Hinj. split; intros Heq.
-    - apply gmultiset_leibniz; intros x.
-      rewrite <- !multiplicity_gmultiset_map with f _ _; [|done|done].
-      by rewrite Heq.
-    - by subst.
+    intros Hinj. intros X Y Heq.
+    apply gmultiset_leibniz; intros x.
+    rewrite <- !multiplicity_gmultiset_map with f _ _; [|done|done].
+    by rewrite Heq.
   Qed.
 
   Global Instance set_unfold_gmultiset_map f X (P : A → Prop) y :
-- 
GitLab