proposition: Lemma compare_g2h (a beta : T1): compare (g2h a) (g2h beta) = compare a beta .
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0) Coq(Relations Basics Wellfounded.Inverse_Image Wellfounded.Inclusion)