proposition: Lemma L_limE alpha i : E0limit alpha -> L_ alpha i = L_ (E0Canon alpha i) (S i).
proof: Proof. move => Halpha; rewrite /E0limit /L_ L_alpha.L_lim_eqn /E0Canon. - congr L_alpha.L_; apply E0_eq_intro; cbn; by rewrite g2h_canon. - move: Halpha ; by rewrite /E0limit. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder) hydras(T1 E0) hydras(L_alpha) gaia_hydras(T1Bridge GCanon GPaths GHprime)