proposition: Lemma cnf_Cons (alpha beta: E0) n : alpha <> E0zero -> beta o< E0_phi0 alpha -> cnf (Cons alpha n beta) = cons (cnf alpha) n (cnf beta).
proof: Proof. intros. unfold Cons. rewrite Omega_term_plus; auto. Defined.
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)