proposition: Lemma isapropis2binophrel {X : setwith2binop} (R : hrel X) : isaprop (is2binophrel R).
proof: Proof. apply (isofhleveldirprod 1). - apply isapropisbinophrel. - apply isapropisbinophrel. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions