proposition: Lemma f_star_zero_eqn : forall alpha i, f_star (alpha, 0) i = i.
proof: Proof. intros; now rewrite f_star_equation_1. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)