Introduce `SingletonMS` class for multiset singletons.

• Define set-like notation {[+ x1; ..; xn ]} for multisets in terms of the new singleton class and disjoint union ⊎.
• Remove SemiSet instance for multisets.
• Prove lemmas regarding ∈ and ∉ for multisets since we no longer get the generic versions for sets.
• Provide SetUnfoldElemOf instances for multisets since we no longer get the generic versions for sets.
• Prove lemmas new regarding ∈ and ∉ for ∩

Fixes #100 (closed), #98 (closed) and #87 (closed).

This MR is an alternative to !232 (closed).