proposition: Lemma mVariant: Hvariant nf_Wf free m .
proof: Proof. split; move => i h h' Hnot_head step; rewrite /restrict; split. 1,3 : apply m_nf. rewrite -(h2g_g2hK (m h)) -(h2g_g2hK (m h')). apply lt_ref; rewrite !m_ref; by apply round_decr. 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