proposition: Lemma F_zeroE i: F_ E0zero i = i.+1.
proof: Proof. rewrite /F_; replace (E0_g2h E0zero) with E0.E0zero. - by rewrite F_zero_eqn. - apply E0_eq_intro => //. 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)