proposition: Lemma H'_omega_cube : forall k, H'_ (E0_phi0 3)%e0 k = iterate (H'_ (E0_phi0 2)) (S k) k.
proof: Proof. intro k; rewrite <- FinS_eq, -> FinS_Succ_eq, H'_Phi0_succ; auto. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)