proposition: Lemma multiset2list_empty : multiset2list empty = nil.
proof: Proof. unfold multiset2list. elim (mult_to_list empty). intros x Hx; destruct x as [ | a x]; trivial. gen (meq_sym Hx); clear Hx; intro Hx. gen (union_isempty Hx); clear Hx; intro Hx. elim (singleton_notempty Hx). Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)