proposition: Lemma member_insert a M : a in (insert a M).
proof: Proof. apply member_union_l. apply singleton_member. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)