Fix pretty printing of multset literals + add tests

See merge request iris/stdpp!253

Introduce `SingletonMS` class for multiset singletons.

Closes #100, #98, and #87

See merge request iris/stdpp!251

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

Fix inconsistent arguments of `subset_difference_elem_of`.

See merge request iris/stdpp!252

Add list_to_map_app

See merge request iris/stdpp!249

Add tactic `learn_hyp`, fixes #73

Closes #73

See merge request iris/stdpp!247

Add lemmas about testbit on bounded integers

See merge request iris/stdpp!248

More lemmas for list's prefix_of and suffix_of

See merge request iris/stdpp!239

Add lemma `lookup_app`, and derive other `lookup_app` lemmas from it.

See merge request iris/stdpp!243

Add more typeclasses

See merge request iris/stdpp!246

Add lemma `lookup_map_seq`, derive other `lookup_map_seq` lemmas from that.

See merge request iris/stdpp!242

Hint Mode Equiv: update link to blocking Coq issue

See merge request iris/stdpp!241

Based on
https://github.com/coq/coq/issues/9058#issuecomment-496479506.

Future proof rotate_nat_add_add_mod

See merge request iris/stdpp!240

surjective_finite

See merge request !238