From 8b97a7e0d85c62c15423eb3fb99b9c4bfa98da27 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 26 Jul 2021 20:34:41 +0200
Subject: [PATCH] Add `gmultiset_singleton_subseteq`.

---
 theories/gmultiset.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 075af94c..46486b49 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.
-- 
GitLab