proposition: Lemma H'_eq2 alpha i : H'_ (E0_succ alpha) i = H'_ alpha (S i).
proof: Proof. rewrite H'_eq2_0. - now rewrite E0_pred_of_Succ. - apply Succ_Succb. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)