proposition: Lemma Lemma5 : forall alpha, P alpha.
proof: Proof. intro alpha; apply transfinite_induction; red. clear alpha; intro alpha; destruct (zero_or_positive alpha). subst; intros _; apply Lemma5_0. intro; apply induct_step; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)