fact: Fixpoint gamma_ (n:nat) : Ord := match n with O => succ beta | S n => sup (fun (y : Ord) => exists xi: Ord, xi < alpha /\ y = phi xi (gamma_ n)) end.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)