Lemma isapropisbinophrel {X : setwithbinop} (R : hrel X) : isaprop (isbinophrel R). 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.