fact: Definition lt {n:nat} : relation (t n) := fun alpha beta => Nat.ltb (proj1_sig alpha) (proj1_sig beta).
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)