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