proposition: Lemma F_alpha_Succ_le alpha: fun_le (F_ alpha) (F_ (E0_succ alpha)).
proof: Proof. rewrite /fun_le /F_ g2h_E0_succ => n; apply /leP; apply F_alpha_Succ_le. 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)