proposition: Lemma H'_Phi0_succ alpha : forall k, H'_ (E0_phi0 (E0_succ alpha)) k = H'_succ_fun (H'_ (E0_phi0 alpha)) k.
proof: Proof. destruct (E0_eq_dec alpha E0zero). - subst; apply H'_Phi0_succ_0. - now apply H'_Phi0_succ_1. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)