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