proposition: Lemma finite_empty : finite empty.
proof: Proof. rewrite empty_of_list. apply finite_of_list. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)