diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 15c9b648d1cf1cb69934ce20775106095b5ffde5..f7040a817415b5593b527d9f23d036d259523190 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.