proposition: Lemma L_eq2 alpha i : E0is_succ alpha -> L_ alpha i = L_ (E0_pred alpha) (S i).
proof: Proof. intros; rewrite L__equation_1; destruct (E0_eq_dec alpha E0zero). - subst; discriminate. - cbn; destruct (Utils.dec (E0limit alpha)) . apply Succ_not_T1limit in H; destruct H; auto. now cbn. Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)