proposition: Lemma L_zero_eqn : forall i, L_ E0zero i = i.
proof: Proof. intro i; now rewrite L__equation_1. Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)