proposition: Lemma succ_injection (alpha beta : Ord) : succ alpha = succ beta -> alpha = beta.
proof: Proof. intros H; tricho alpha beta t;auto. - generalize (succ_mono t). rewrite H; intro; case (@lt_irrefl (succ beta));auto. - generalize (succ_mono t). rewrite H; intro; case (@lt_irrefl (succ beta));auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)