proposition: Lemma L_eq2 alpha i : E0is_succ alpha -> L_ alpha i = L_ (E0_pred alpha) (S i).
proof: Proof. move => H; case (E0is_succE H) => x Hx; subst. rewrite E0_pred_succK /L_ L_alpha.L_eq2 => //. congr L_alpha.L_; rewrite g2h_E0_succ; by rewrite E0_pred_of_Succ. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder) hydras(T1 E0) hydras(L_alpha) gaia_hydras(T1Bridge GCanon GPaths GHprime)