proposition: Lemma Omega_term_plus alpha beta i : alpha <> E0zero -> (beta o< E0_phi0 alpha)%e0 -> cnf (Omega_term alpha i + beta)%e0 = cons (cnf alpha) i (cnf beta).
proof: Proof. destruct alpha as [alpha Halpha]; destruct beta as [beta Hbeta]. intros. unfold lt in H0. simpl in H0. unfold Omega_term. unfold cnf. unfold E0add. unfold cnf at 1 2. fold (omega_term alpha i ). rewrite omega_term_plus_rw. reflexivity. rewrite nf_LT_iff; tauto. 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)