From fde7718b45a3dd4d16401f054a4501d41e7ac179 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Apr 2021 10:49:43 +0200
Subject: [PATCH] Add lemma `gmultiset_not_elem_of_empty`.

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

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index ba37efe1..c07aa6c3 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -370,6 +370,8 @@ Section more_lemmas.
   Proof. multiset_solver. Qed.
 
   (** Element of operation *)
+  Lemma gmultiset_not_elem_of_empty x : x ∉@{gmultiset A} ∅.
+  Proof. multiset_solver. Qed.
   Lemma gmultiset_not_elem_of_singleton x y : x ∉@{gmultiset A} {[+ y +]} ↔ x ≠ y.
   Proof. multiset_solver. Qed.
   Lemma gmultiset_not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
-- 
GitLab