proposition: Lemma H'_eq2_0 alpha i : E0is_succ alpha -> H'_ alpha i = H'_ (E0_pred alpha) (S i).
proof: Proof. intros;rewrite H'__equation_1. destruct (E0_eq_dec alpha E0zero). - subst; discriminate. - cbn; destruct (Utils.dec (E0limit alpha)) . destruct (Succ_not_T1limit _ H); auto. + now cbn. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)