proposition: Lemma H'_Phi0_succ_1 alpha : alpha <> E0zero -> forall k, H'_ (E0_phi0 (E0_succ alpha)) k = H'_succ_fun (H'_ (E0_phi0 alpha)) k.
proof: Proof. Proof with auto with E0. intros; unfold H'_succ_fun ; rewrite H'_eq3, CanonS_Phi0_Succ_eqn, H'_Omega_term ... Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)