proposition: Lemma finite_add a P : finite P -> finite (add a P).
proof: Proof. destruct (classic (mem a P)). intro P_fin. rewrite add_already_in; hyp. rewrite finite_eq; intros [l e]. rewrite e, <- of_cons. apply finite_of_list. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)