There are two "SubsetEq" instances for gmultiset
We currently have two non-equivalent instances for
SubsetEq for gmultiset, which leads to very confusing situations:
gmultiset_subseteqis the expected instance in terms of multiplicites
- But there also is
set_subseteqwhich is a general instance based on
IMO multisets show that the general instance is undesirable -- from the fact that a type has an
ElemOf instance, we cannot derive how its subset relation ought to look. That instance should likely be removed, and replaced by manual instances for types that actually want it.
FWIW, the same applies to the general
set_equiv. I am not sure about
set_disjoint... that one is correct for multisets, so maybe we can keep it at least for now. "No element is in both sets" seems like a reasonable definition for disjointness for anything that has membership.