proposition: Lemma m_ref h : g2h (m h) = (Hydra_Termination.m h).
proof: Proof. induction h using Hydra_rect2 with (P0 := (fun hs => g2h (ms hs) = Hydra_Termination.ms hs)) => //. - case: h IHh => [/= // |] => h hs H => //. - rewrite /ms -!/m -!/ms /oplus g2h_phi0 IHh IHh0 g2h_h2gK => //. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic) hydras(T1 E0 Hessenberg Hydra_Theorems Hydra_Definitions Hydra_Termination Battle_length Hydra_Examples Epsilon0_Needed_Free Epsilon0_Needed_Std) T1Bridge GHessenberg GL_alpha GPrelude