proposition: Lemma F_succE alpha i : F_ (E0_succ alpha) i = Iterates.iterate (F_ alpha) i.+1 i.
proof: Proof. rewrite (Iterates.iterate_ext _ (F_alpha.F_ (E0_g2h alpha))); last first. by rewrite /F_. rewrite -F_succ_eqn /F_. congr hF_; apply E0_eq_intro => /= ; by rewrite g2h_succ. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec Arith) hydras(DecPreOrder) hydras(T1 E0) hydras(primRec) hydras(F_alpha F_omega) gaia_hydras(T1Bridge GCanon GHprime)