proposition: Lemma Cr_pos_iff (alpha : Ord) : zero < alpha -> forall x, (Cr alpha x <-> (forall beta (H:beta < alpha), In (A_ beta) x /\ phi beta x = x)).
proof: Proof. split. - intros; apply Cr_pos_inv with alpha; auto. - intros; apply Cr_pos; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)