proposition: Lemma HF0 : P E0zero.
proof: Proof. intro n; rewrite F_zero_eqn. replace (E0_phi0 E0zero) with (E0fin 1). - now rewrite H'_Fin. - now apply E0_eq_intro. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)