proposition: Lemma empty_card : card empty = 0.
proof: Proof. intros. unfold card. destruct (card_def empty); simpl. rewrite <- e. rewrite multiset2list_empty; trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)