proposition: Lemma singleton_card x : card {{x}} = 1.
proof: Proof. unfold card. destruct (card_def {{x}}); simpl. rewrite <- e. destruct (multiset2list_singleton x) as [x' [_ xx']]. rewrite xx'; trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)