proposition: Lemma finite_diff P : finite P -> forall Q, finite (diff P Q).
proof: Proof. rewrite finite_eq. intros [l Pl]. intro Q. rewrite finite_eq. ex (select (fun x => dec (~mem x Q)) l). split; intro hx. apply select_complete; fo. unfold mem, of_list in hx. apply select_correct in hx. fo. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)