proposition: Lemma L_ok (alpha: E0) : P alpha.
proof: Proof. Proof with eauto with E0. apply well_founded_induction with E0lt ... clear alpha; intros alpha IHalpha. destruct (Zero_Limit_Succ_dec alpha) as [[H | H] | H]. - subst; apply L_ok0. - apply L_ok_lim; auto. - destruct H as [beta Hbeta]; subst; apply L_ok_succ. apply IHalpha; auto with E0. Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)