proposition: Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
proof: Proof. intro x; rewrite <- Empty_set_zero'. apply Union_is_finite; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat