proposition: Theorem Add_preserves_Finite : forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
proof: Proof. intros X x H'. elim (classic (In U X x)); intro H'0; auto with sets. rewrite (Non_disjoint_union U X x); auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat