proposition: Lemma Succ_of_cons alpha gamma i : alpha <> E0zero -> gamma o< E0_phi0 alpha -> cnf (E0_succ (Omega_term alpha i + gamma)%e0) = cnf (Omega_term alpha i + E0_succ gamma)%e0.
proof: Proof. intros. rewrite Omega_term_plus; auto. rewrite Succ_rw. rewrite Omega_term_plus; auto. rewrite succ_cons', Succ_rw; auto. intro H1; apply H, E0_eq_intro. assumption. destruct H0. destruct H1. rewrite cnf_phi0 in H1. apply nf_intro; auto. now apply lt_a_phi0_b_phi0R. red. apply succ_lt_limit. rewrite cnf_phi0. apply nf_phi0. apply cnf_ok. rewrite cnf_phi0. simpl. case_eq (cnf alpha). intro. destruct H. apply E0_eq_intro. assumption. intros; trivial. now red. assumption. 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)