proposition: Lemma phi0_well_named : forall alpha, phi0 alpha = phi 0 alpha.
proof: Proof. intro alpha;unfold phi, finite; now rewrite Cr_zero_AP. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)