proposition: Lemma F_alpha_not_PR_E0 alpha: E0le E0_omega alpha -> isPR 1 (F_ alpha) -> False.
proof: Proof. move => Halpha HPR; have H0: isPR 1 (F_alpha.F_ (E0_g2h alpha)). eapply isPRextEqual with (F_ alpha) => //. eapply F_alpha_not_PR with (E0_g2h alpha) => //. replace E0.E0_omega with (E0_g2h E0_omega); last first. - by apply E0_eq_intro. - by rewrite -gE0le_iff. 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)