proposition: Lemma countable_members (alpha : Ord): Countable (members alpha).
proof: Proof. apply AX2; now exists alpha. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)