proposition: Lemma L_finite : forall i k :nat, L_ (E0fin i) k = (i+k)%nat.
proof: Proof. move => i k. by rewrite /L_ E0g2h_Fin L_alpha.L_finite. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder) hydras(T1 E0) hydras(L_alpha) gaia_hydras(T1Bridge GCanon GPaths GHprime)