• Robbert Krebbers's avatar
    Introduce `SingletonMS` class for multiset singletons. · 0120e6fa
    Robbert Krebbers authored
    - 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.
    0120e6fa
multiset_solver.v 2.86 KB