proposition: Lemma phi0_sup : forall U: Ensemble Ord, Inhabited U -> Countable U -> phi0 (|_| U) = |_| (image U phi0).
proof: Proof. intros U H0 H1; case normal_phi0. destruct 2 as [H2 [H3 H4]]; symmetry; auto. apply H4; auto; split. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)