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