fact: Definition ispartinvbinophrel {X : setwithbinop} (S : hsubtype X) (R : hrel X) : UU := dirprod (∏ a b c : X, S c -> R (op c a) (op c b) -> R a b) (∏ a b c : X, S c -> R (op a c) (op b c) -> R a b).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions