GitLab

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. and apply 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.