proposition: Lemma T1limit_phi0 alpha : alpha <> E0zero -> E0limit (E0_phi0 alpha).
proof: Proof. unfold E0_phi0; apply T1limit_Omega_term. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)