Draft: Drop misleading gmultiset_simple_set instance
The problem is that elem_of_subseteq_singleton applies to multiset goals, but uses the wrong instance.
[...] when my goal is a multiset elem-of, then
apply gmultiset_elem_of_singleton_subseteq.andapply elem_of_subseteq_singleton.result in different goals that print exactly the same (also btw note the inconsistent lemma name)
Based on a suggestion by Robbert (which I might have misunderstood); but I'm not sure this is the right fix.
This instance appears to not be used, and it allows applying lemmas like elem_of_subseteq_singleton which are inappropriate for gmultiset, as they use the set_subseteq instance for SubsetEq, instead of gmultiset_subseteq : SubsetEq (gmultiset A).
However, the lemmas should be restated in terms of gmultiset, since they do hold, and they hold on sensible instances.