proposition: Lemma finite_dec : forall P:set, finite P -> dec P.
proof: Proof. red; intros P FP; elim FP; intros. right; intro; apply (equiv_empty_false x e); auto. case (e x0); unfold add; intuition. case (X x0); intuition. case (decA x0 x); intuition. Qed.
imports: Coq(Arith) Coq(Lt)