Add `Proper`s for maps, and generalise existing ones. Add tests to check that the old ones can be derived.

- 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, #98 and #87.

This MR is an alternative to !232.

Turn `x ∈ X` only into `0 < multiplicity x X` at leaves of `∈` to enable better first-order reasoning.

Extracted from iris/iris!409.