`Equivalence` for `≡` on gmultisets.
Showing
...  @@ 45,7 +45,7 @@ Section definitions.  ...  @@ 45,7 +45,7 @@ Section definitions. 
Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,  Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,  
let (X) := X in dom _ X.  let (X) := X in dom _ X.  
End definitions.  End definitions.  


Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.  Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.  
Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.  Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.  
...  @@ 66,6 +66,8 @@ Proof.  ...  @@ 66,6 +66,8 @@ Proof. 
Qed.  Qed.  
Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).  Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).  
Proof. intros X Y. by rewrite gmultiset_eq. Qed.  Proof. intros X Y. by rewrite gmultiset_eq. Qed.  
Global Instance gmultiset_equivalence : Equivalence (≡@{gmultiset A}).  
Proof. constructor; repeat intro; naive_solver. Qed.  
(* Multiplicity *)  (* Multiplicity *)  
Lemma multiplicity_empty x : multiplicity x ∅ = 0.  Lemma multiplicity_empty x : multiplicity x ∅ = 0.  
...  ... 