elem_of_intersection not applicable to multisets

I believe that the lemma elem_of_intersection should in principle be applicable to multisets, since the property x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y is true on multisets. Unfortunately, the current statement of this lemma includes the type class constraint Set_ A C, which cannot be satisfied by multisets, because this type class includes the property elem_of_difference, that is, x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y, which is not satisfied by multisets.

It seems to me that it should be possible to fix this issue, without breaking backward compatibility, by inserting a new type class in between SemiSet and Set_.