proposition: Lemma H'_F alpha n : (F_ alpha n.+1 <= H'_ (E0_phi0 alpha) n.+1)%N.
proof: Proof. apply /leP; rewrite /F_ /H'_. replace (E0_g2h (E0_phi0 alpha)) with (hE0phi0 (E0_g2h alpha)). - apply H'_F; apply E0_eq_intro; destruct alpha => /=. - apply E0_eq_intro; rewrite /E0_phi0 => //. 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)