proposition: Lemma CanonS_Phi0_Succ_eqn i gamma: Canon (E0_phi0 (E0_succ gamma)) (S i) = Omega_term gamma i.
proof: Proof. apply E0_eq_intro; unfold Canon. rewrite cnf_rw, cnf_Omega_term, cnf_phi0, cnf_Succ. rewrite canonS_phi0_succ_eqn; auto with E0. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)