proposition: Lemma members_eq (alpha beta : Ord) : members alpha = members beta -> alpha = beta.
proof: Proof. intros H; tricho alpha beta H2; auto with schutte. - assert (H0: members beta alpha) by auto. rewrite <- H in H0; destruct (lt_irrefl H0);auto. - assert (H0: members alpha beta) by auto. rewrite H in H0; destruct (lt_irrefl H0);auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)