diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index b72865c8075d5983e9e074fde34a4820b5e57619..6cf5d9404f92739bcdd700deb23e98cfb2b2a597 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 :