proposition: Lemma f_lim_eqn : forall alpha i, E0limit alpha -> f_ alpha i = f_ (Canon alpha i) i.
proof: Proof. unfold f_; intros. rewrite f_star_equation_2. destruct (E0_eq_dec alpha E0zero). - now destruct (Limit_not_Zero H). - cbn; destruct (Utils.dec (E0limit alpha)) . + cbn; auto. + red in H; rewrite e in H; discriminate. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)