proposition: Lemma F_star_iterate : forall alpha n i, F_star (alpha, n) i = iterate (F_ alpha) n i.
proof: Proof. induction n; intro i; simpl. - now rewrite F_star_zero_eqn. - specialize (IHn i); rewrite F_star_Succ in *; now rewrite <- IHn. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)