proposition: Lemma A_Cr (alpha beta:Ord) : In (A_ alpha) beta -> phi alpha beta = beta -> In (Cr alpha) beta.
proof: Proof. unfold A_; intros H H0; rewrite <- H0. unfold phi; destruct (ord_ok (Cr alpha)). specialize (OF_total _ H); auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)