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

theories/gmultiset.v

@@ -119,15 +119,6 @@ Section basic_lemmas.
   Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X.
   Proof. done. Qed.
 
-  Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
-  Proof.
-    split.
-    - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
-    - intros x y.
-      rewrite elem_of_multiplicity, multiplicity_singleton'.
-      destruct (decide (x = y)); intuition lia.
-    - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
-  Qed.
   Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
   Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
 

[Ralf Jung]

Ah, so this way we have two "subseteq" instances, I see.

Maybe add a comment explaining that this instance deliberately does not exist?