From f0d5ebf077c3dcda7dac0f398f713f91b52e8baa Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 26 Jul 2021 20:33:50 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20`gmultiset=5Felem=5Fof=5Fsingleton=5Fs?=
 =?UTF-8?q?ubseteq`=20=E2=86=92=20`gmultiset=5Fsingleton=5Fsubseteq=5Fl`?=
 =?UTF-8?q?=20and=20swap=20order=20to=20be=20consistent=20with=20Iris's=20?=
 =?UTF-8?q?`singleton=5Fincluded=5Fl`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/gmultiset.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index bb799aba..075af94c 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -568,7 +568,7 @@ Section more_lemmas.
   Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ⊎ Y.
   Proof. multiset_solver. Qed.
 
-  Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[+ x +]} ⊆ X.
+  Lemma gmultiset_singleton_subseteq_l x X : {[+ x +]} ⊆ X ↔ x ∈ X.
   Proof. multiset_solver. Qed.
 
   Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
-- 
GitLab