proposition: Lemma card_of_list_eq_length l : nodup l -> card (Pf_of_list l) = length l.
proof: Proof. apply card_of_list_eq_length_gen. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)