proposition: Theorem P_alpha : forall alpha, P alpha.
proof: Proof. intro alpha; apply well_founded_induction with E0lt. - exact E0lt_wf. - apply P_alpha_0. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)