proposition: Lemma F_succ_eqn : forall alpha i, F_ (E0_succ alpha) i = iterate (F_ alpha) (S i) i.
proof: Proof. Proof with auto with E0. intros;rewrite F_eq2, F_star_iterate ... - now rewrite E0_pred_of_Succ. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)