fact: Definition restrict (T : finType) (P : pred T) (Tp : subType P) (e : rel T) := fun x y : Tp => e (val x) (val y).
imports: Relations Recdef mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base)