proposition: Lemma Cr_1_iff (alpha : Ord): Cr 1 alpha <-> AP alpha /\ phi0 alpha = alpha.
proof: Proof. generalize (Cr_pos_inv (alpha := F 1)). intro H; assert (H01 : zero < F 1). { simpl; apply lt_succ; split. } split. + intros H0; generalize (H H01 alpha H0). intros H1; generalize (H1 zero H01). intros (H5,H6); split. * rewrite <- H6; rewrite <- phi0_well_named. apply AP_phi0. * unfold _phi0; replace AP with (Cr zero); auto. apply Extensionality_Ensembles. split. { red; red; intros x H2. red; intros; apply Cr_zero_inv; auto. } { red; red; intros;apply Cr_zero; auto. } + intros (H2,H3); apply Cr_pos; auto. split. * intros; assert (beta=zero). { simpl in H0; generalize (lt_succ_le_2 zero H0). intro H4;rewrite (le_alpha_zero H4); trivial. } subst beta; red. rewrite Cr_zero_AP, AP_o_segment. split. * rewrite phi0_well_named in H3. assert (beta=zero). { simpl in H0; generalize (lt_succ_le_2 zero H0). intro H4;rewrite (le_alpha_zero H4); auto. } subst beta; unfold phi in H3; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)