proposition: Lemma Cr_pos : forall alpha, zero < alpha -> forall x : Ord , (forall beta (H:beta < alpha), A_ beta x /\ ord (Cr beta) x = x) -> Cr alpha x.
proof: Proof. intros; rewrite Cr_equation; right . split; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)