proposition: Lemma H'_eq3 alpha i : E0limit alpha -> H'_ alpha i = H'_ (E0Canon alpha (S i)) i.
proof: Proof. rewrite /E0limit /H'_ => H; rewrite H'_eq3 => //; congr Hprime.H'_. apply E0_eq_intro => /=; by rewrite g2h_canon. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder T1 E0) hydras(Iterates Hprime L_alpha) gaia_hydras(T1Bridge GCanon GPaths)