proposition: Lemma all_ord_acc : forall alpha : Ord, Acc lt alpha.
proof: Proof. intros alpha ; pattern alpha; apply transfinite_induction; auto. apply Progressive_Acc; auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)