proposition: Lemma fstar_S : forall alpha n i, f_star (alpha, S (S n)) i = f_ alpha (f_star (alpha, S n) i).
proof: Proof. unfold F_; intros; now rewrite f_star_equation_3. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)