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