proposition: Lemma finite_of_list l : finite (of_list l).
proof: Proof. assert (e : of_list l [=] of_list (remdup eq_dec l)). intro x. unfold mem, of_list. sym. apply In_remdup. rewrite e. apply finite_of_list_nodup. apply nodup_remdup. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)