proposition: Lemma finite_surj P n (f : N n -> elts P) : surjective f -> finite P.
proof: Proof. intro f_surj. rewrite (of_map_L f_surj). apply finite_of_list. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)