proposition: Lemma CanonSSn (i:nat) : forall alpha n , alpha <> E0zero -> Canon (Cons alpha (S n) E0zero) (S i) = Cons alpha n (Canon (E0_phi0 alpha) (S i)).
proof: Proof. intros; apply E0_eq_intro. unfold Canon; repeat (rewrite cnf_rw || rewrite cnf_Cons); auto. - rewrite canon_SSn_zero; auto with E0. - unfold lt, E0_phi0; repeat rewrite cnf_rw. apply canonS_LT ; trivial. apply nf_phi0;auto with E0. discriminate. - unfold lt; eauto with E0. apply LT1; apply nf_phi0;auto with E0. Qed.
imports: hydras.Prelude(DecPreOrder) hydras(Fuel)