proposition: Lemma F_limE alpha i: T1limit (cnf alpha) -> F_ alpha i = F_ (E0Canon alpha i) i.
proof: Proof. move => Hlimit; rewrite /F_ F_lim_eqn. - congr hF_; apply E0_eq_intro; cbn; by rewrite g2h_canon. - rewrite /hE0limit T1limit_ref. move: alpha Hlimit ;case => /= x Hx H'x; by rewrite h2g_g2hK. 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)