proposition: Lemma LE_ref : refinesRel T1.LE LE.
proof: Proof. split. - case => a b; split. + rewrite -nf_ref => //. + case: b => c _; case :c => [y0 Hy0 |]. apply T1ltW. * rewrite - decide_hltE => //. red; rewrite bool_decide_eq_true => //. * apply T1lenn. + case b => _ ?; rewrite - nf_ref => //. - case; rewrite /T1.LE; repeat split => //. + move: p p1; rewrite -nf_ref => //. + move: p0; rewrite T1le_eqVlt => /orP. case => /eqP Heq; subst. * move: Heq; rewrite h2g_eqE => ?; subst; right. * left; move: Heq; rewrite -decide_hltE => // Heq. move: Heq => /eqP; rewrite bool_decide_eq_true => //. + move: p1 ; rewrite -nf_ref => //. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)