proposition: Lemma H'_Phi0_Si : forall i k, H'_ (E0_phi0 (S i)) k = iterate H'_succ_fun i (H'_ E0_omega) k.
proof: Proof. Proof with auto with E0. induction i. - simpl; replace (E0_phi0 (E0finS 0)) with E0_omega; auto; orefl. - intro k; rewrite <- FinS_eq, FinS_Succ_eq. rewrite H'_Phi0_succ, iterate_S_eqn. apply iterate_ext; auto. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)