proposition: Lemma f_zero_eqn : forall i, f_ E0zero i = S i.
proof: Proof. intro i. unfold f_; rewrite f_star_equation_2. destruct (E0_eq_dec E0zero E0zero). - now cbn. - now destruct n. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)