fact: Fixpoint list_to_multiset (l : list elt) {struct l} : multiset elt := match l with | nil => EmptyBag elt | h :: tl => munion (SingletonBag _ eq_elt_dec h) (list_to_multiset tl) end.
imports: decidable_set List more_list Multiset Arith Setoid