proposition: Lemma Cr_pos_inv (alpha : Ord) : zero < alpha -> forall x, Cr alpha x -> (forall beta (H:beta < alpha), In (A_ beta) x /\ phi beta x = x).
proof: Proof. intros H x H0 beta H1; case (Cr_inv alpha x H0). - destruct 1; subst alpha; case (@not_lt_zero beta); auto. - destruct 1; eauto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)