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