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