proposition: Lemma isapropisbinophrel {X : setwithbinop} (R : hrel X) : isaprop (isbinophrel R).
proof: Proof. apply isapropdirprod. - apply impred. intro a. apply impred. intro b. apply impred. intro c. apply impred. intro r. apply (pr2 (R _ _)). - apply impred. intro a. apply impred. intro b. apply impred. intro c. apply impred. intro r. apply (pr2 (R _ _)). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions