proposition: Lemma T1limit_Omega_term alpha i : alpha <> E0zero -> E0limit (Omega_term alpha i).
proof: Proof. intro H; unfold E0limit; destruct alpha as [cnf0 H0]; cbn; destruct cnf0. - destruct H; auto with E0. - red; trivial. 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)