proposition: Lemma CanonS_phi0_Succ alpha i : Canon (E0_phi0 (E0_succ alpha)) (S i) = Omega_term alpha i.
proof: Proof. apply E0_eq_intro; unfold Omega_term, E0_phi0, E0_succ. simpl cnf; rewrite pred_of_succ; case_eq (succ (cnf alpha)). - intro H; destruct (succ_not_zero _ H); auto. - reflexivity. - intro; apply cnf_ok. - intros; apply cnf_ok. Qed.
imports: hydras.Prelude(DecPreOrder) hydras(Fuel)