diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index c07aa6c3e93ed6ee150d65a12d723e047b5d00fd..311ded6ec5cc15e8b197cc63e52d2158964a1e37 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -380,6 +380,12 @@ Section more_lemmas.
   Proof. multiset_solver. Qed.
 
   (** Misc *)
+  Global Instance gmultiset_singleton_inj : Inj (=) (=@{gmultiset A}) singletonMS.
+  Proof.
+    intros x1 x2 Hx. rewrite gmultiset_eq in Hx. specialize (Hx x1).
+    rewrite multiplicity_singleton, multiplicity_singleton' in Hx.
+    case_decide; [done|lia].
+  Qed.
   Lemma gmultiset_non_empty_singleton x : {[+ x +]} ≠@{gmultiset A} ∅.
   Proof. multiset_solver. Qed.
 
diff --git a/theories/sets.v b/theories/sets.v
index f37e6869c67faeacf6dfa8ccc126ee2e94bc6621..984e667cae0d3711fc0c55bfed32df08ee6c2e4b 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -364,6 +364,10 @@ Section semi_set.
   Proof. set_solver. Qed.
   Lemma set_equiv_subseteq X Y : X ≡ Y ↔ X ⊆ Y ∧ Y ⊆ X.
   Proof. set_solver. Qed.
+  Global Instance singleton_equiv_inj : Inj (=) (≡@{C}) singleton.
+  Proof. unfold Inj. set_solver. Qed.
+  Global Instance singleton_inj `{!LeibnizEquiv C} : Inj (=) (=@{C}) singleton.
+  Proof. unfold Inj. set_solver. Qed.
 
   (** Subset relation *)
   Global Instance set_subseteq_antisymm: AntiSymm (≡) (⊆@{C}).