proposition: Lemma members_omega : Same_set (members omega) is_finite.
proof: Proof. unfold Same_set;split; red; unfold members, In. - intros x Hx; case (lt_omega_finite Hx); intros x0; exists x0; auto. - destruct 1 as [n [_ Hn]]; subst ;auto with schutte. apply finite_lt_omega. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)