From 793110fe0ca8ec09e92cc1b3c698d63f2f56c1e3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Apr 2018 10:34:37 +0200
Subject: [PATCH] =?UTF-8?q?`Equivalence`=20for=20`=E2=89=A1`=20on=20gmulti?=
 =?UTF-8?q?sets.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/gmultiset.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 15c9b648..f7040a81 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -45,7 +45,7 @@ Section definitions.
 
   Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
     let (X) := X in dom _ X.
-End definitions.
+End definitions. 
 
 Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
 Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
@@ -66,6 +66,8 @@ Proof.
 Qed.
 Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
 Proof. intros X Y. by rewrite gmultiset_eq. Qed.
+Global Instance gmultiset_equivalence : Equivalence (≡@{gmultiset A}).
+Proof. constructor; repeat intro; naive_solver. Qed.
 
 (* Multiplicity *)
 Lemma multiplicity_empty x : multiplicity x ∅ = 0.
-- 
GitLab