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.