proposition: Lemma F_star_Succ: forall alpha n i, F_star (alpha, S n) i = F_ alpha (F_star (alpha, n) i).
proof: Proof. destruct n. - intros; now rewrite F_star_zero_eqn. - intros i; unfold F_; now rewrite Fstar_S. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)