proposition: Lemma H'_eq2 alpha i : H'_ (E0_succ alpha) i = H'_ alpha (S i).
proof: Proof. case alpha => ? ?; by rewrite /H'_ g2h_E0_succ H'_eq2. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder T1 E0) hydras(Iterates Hprime L_alpha) gaia_hydras(T1Bridge GCanon GPaths)