proposition: Lemma L_succ_eqn alpha i : L_ (E0_succ alpha) i = L_ alpha (S i).
proof: Proof. intros;rewrite L_eq2; [autorewrite with E0_rw using trivial | auto with E0]. Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)