proposition: Lemma F_eq2 : forall alpha i, E0is_succ alpha -> F_ alpha i = F_star (E0_pred alpha, S i) i.
proof: Proof. unfold F_; intros; rewrite F_star_equation_2. destruct (E0_eq_dec alpha E0zero). - subst alpha; discriminate H. - cbn; destruct (Utils.dec (E0limit alpha)) . + assert (true=false) by ( now destruct (Succ_not_T1limit _ H)). discriminate. + now cbn. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)