proposition: Lemma L_ok_succ beta : P beta -> P (E0_succ beta).
proof: Proof. Proof with auto with E0. intro H; red; rewrite Succ_rw. destruct (E0_eq_dec beta E0zero). - subst; simpl; generalize (L_fin_ok 1); unfold L_fin. replace one with (T1nat 1); [simpl | trivial]. intro; eapply L_spec_compat; eauto. intros; rewrite L_eq2; auto with E0. rewrite E0_pred_of_Succ, L_zero_eqn; trivial. - apply L_spec_compat with (L_succ (L_ beta)); auto. + apply L_succ_ok; auto. * apply cnf_ok; auto. * intro k; apply L_ge_S; auto. + unfold L_succ; intro n0; now autorewrite with L_rw. Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)