proposition: Lemma LF3_2: Iterates.dominates_from 2 (F_ (E0fin 3)) (fun n : nat => Iterates.iterate Exp2.exp2 n.+1 n).
proof: Proof. rewrite /dominates_from /F_. replace (E0_g2h (E0fin 3)) with (hE0fin 3); last first. - by apply E0_eq_intro. - apply LF3_2. 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)