proposition: Lemma Cr_equation (alpha : Ord) : Cr alpha = Cr_fun (fun (y : Ord) (h : y < alpha) => Cr y).
proof: Proof. generalize (@Fix_eq Ord lt all_ord_acc (fun _ : Ord => Ensemble Ord)); intros H; apply (H Cr_fun Cr_extensional alpha). Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)