proposition: Lemma finite_singleton a : finite (singleton a).
proof: Proof. unfold singleton. apply finite_add. apply finite_empty. Defined.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)