proposition: Remark Phi0_def : E0_phi0 2 = ltac:(mko (T1omega * T1omega)%t1).
proof: Proof. apply E0_eq_intro. reflexivity. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)