proposition: Lemma phi0_of_limit (alpha : Ord) : is_limit alpha -> phi0 alpha = |_| (image (members alpha) phi0).
proof: Proof. intro H; pattern alpha at 1; rewrite (is_limit_sup_members H); destruct normal_phi0 as [H0 H1]. destruct H1 as [H1 H2] ;symmetry;auto. destruct H2 as [H2 H3]; apply H3. - intro; split. - exists zero; tricho zero alpha HH; auto. + subst alpha; destruct H as [H _]; now destruct H. + destruct (not_lt_zero HH). - apply countable_members;auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)