proposition: Lemma succ_ok : forall alpha, succ_spec alpha (succ alpha).
proof: Proof. intro alpha; unfold succ, the_least, the; apply iota_spec. destruct (@AX3 (Singleton alpha)). - apply countable_singleton. - unfold succ_spec; apply the_least_unicity; exists x. apply H; split. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)