proposition: Lemma L_succE alpha i : L_ (E0_succ alpha) i = L_ alpha i.+1.
proof: Proof. rewrite L_eq2 ?E0_pred_succK => //; apply E0is_succ_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)