`Inj` instances for set and multiset singletons.

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.
 

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}).