proposition: Lemma Cr_inv (alpha x : Ord): Cr alpha x -> ((alpha = zero /\ (Cr alpha x <-> AP x)) \/ (zero < alpha /\ (forall beta (H:beta < alpha), A_ beta x /\ ord (Cr beta ) x = x))).
proof: Proof. rewrite (Cr_equation alpha); unfold Cr_fun at 1. intros H; case H;auto. case H;intros H0 _. + left; split. * destruct H0; auto. * split. { intro H1; destruct H0;auto. } { intros H1; left; auto. } + auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)