proposition: Lemma finite_eq P : finite P <-> exists l, P [=] of_list l.
proof: Proof. split. intros [n [f [f_inj f_surj]]]. ex (map (elt_val o f) (L n)). apply of_map_L. hyp. intros [l e]. rewrite e. apply finite_of_list. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)