proposition: Lemma card_eq P : card P = length (list_of_finite P).
proof: Proof. rewrite Pf_eq_of_list at 1. rewrite card_of_list_eq_length. refl. apply nodup_list_of_finite. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)