proposition: Lemma H'_cons : forall beta, (beta o< E0_phi0 alpha)%e0 -> forall k, H'_ (Cons alpha i beta) k= H'_ (Omega_term alpha i) (H'_ beta k).
proof: Proof. Proof with auto with E0. unfold Cons; intro beta; pattern beta; apply well_founded_induction with E0lt; clear beta. - exact E0lt_wf. - intros beta Hbeta H; destruct (Zero_Limit_Succ_dec beta). destruct s. + subst; intro k. autorewrite with H'_rw E0_rw using trivial. + intro k; assert (Canon (Omega_term alpha i + beta)%e0 (S k) = (Omega_term alpha i + (Canon beta (S k)))%e0). { rewrite CanonS_plus_1; auto with E0. intro; subst alpha; red in H; simpl in H; apply LT_one in H. unfold E0limit in e; rewrite H in e; discriminate e. } rewrite H'_eq3, H0. specialize (Hbeta (Canon beta (S k))). assert (Canon beta (S k) o< beta)%e0 by auto with E0. assert (Canon beta (S k) o< E0_phi0 alpha)%e0 by (eapply Lt_trans; eauto). now rewrite (Hbeta H1 H2 k), (H'_eq3 beta). apply T1limit_plus; auto. + intro k; destruct s as [gamma Hgamma]; subst. specialize (Hbeta gamma). assert (gamma o< E0_succ gamma)%e0 by (apply Lt_Succ; auto). assert (gamma o< E0_phi0 alpha)%e0 . { apply Lt_trans with (E0_succ gamma); auto. } rewrite (H'_eq2 gamma); replace (Omega_term alpha i + E0_succ gamma)%e0 with (E0_succ (Omega_term alpha i + gamma)%e0). rewrite H'_eq2, Hbeta; auto. apply E0_eq_intro; rewrite Succ_of_cons; auto. intro; subst; red in H; simpl in H. destruct H as [H [H2 H3]]; apply lt_one in H2. destruct (succ_not_zero _ H2). Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)