proposition: Lemma H'_Omega_term (alpha : E0) : forall i k, H'_ (Omega_term alpha i) k = iterate (H'_ (E0_phi0 alpha)) (S i) k.
proof: Proof. destruct (E0_eq_dec alpha E0zero). - subst. intros; replace (Omega_term E0zero i) with (E0fin (S i)). replace (E0_phi0 E0zero) with (E0fin 1). now rewrite H'_Fin_iterate. compute. now apply E0_eq_intro. compute. now apply E0_eq_intro. - intros; now apply H'_Omega_term_0. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)