proposition: Lemma LT_ref : refinesRel T1.LT LT.
proof: Proof. split. - destruct 1 as [H [H0 H1]]; split. + by rewrite -nf_ref. + by apply lt_ref. + by rewrite -nf_ref. - case => H H0 H1; repeat split; red; rewrite ?nf_ref ?lt_ref => // ; by apply lt_ref. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)