diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 075af94c5844ab6d910c51e6a19b0a5edffe07ee..46486b49b33f973a708c89d08bb4b76b3b233418 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -570,6 +570,15 @@ Section more_lemmas.
 
   Lemma gmultiset_singleton_subseteq_l x X : {[+ x +]} ⊆ X ↔ x ∈ X.
   Proof. multiset_solver. Qed.
+  Lemma gmultiset_singleton_subseteq x y :
+    {[+ x +]} ⊆@{gmultiset A} {[+ y +]} ↔ x = y.
+  Proof.
+    split; [|multiset_solver].
+    (* FIXME: [multiset_solver] should solve this *)
+    intros Hxy. specialize (Hxy x).
+    rewrite multiplicity_singleton, multiplicity_singleton' in Hxy.
+    case_decide; [done|lia].
+  Qed.
 
   Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
   Proof. multiset_solver. Qed.