fact: Definition refinesRel (hR: hT1 -> hT1 -> Prop) (gR: T1 -> T1 -> Prop) := forall x y : hT1, hR x y <-> gR (h2g x) (h2g y).
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)