proposition: Lemma singleton_notempty x : {{x}} <>mul empty.
proof: Proof. apply member_notempty with x. apply singleton_member. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)