gmultiset RA
The only weird thing about this PR that I can think of is the
Local Instance gmultiset_equiv : Equiv (gmultiset K) := (=) hack: the RA laws hold only w.r.t. the Leibniz equality, and not the collection equivalence relation.
The only weird thing about this PR that I can think of is the
Local Instance gmultiset_equiv : Equiv (gmultiset K) := (=) hack: the RA laws hold only w.r.t. the Leibniz equality, and not the collection equivalence relation.