Definition binopeqrel_eq (X : setwithbinop) : binopeqrel X. Proof. use make_binopeqrel. - use make_eqrel. + intros x x'. exact (make_hProp (x = x') (pr2 (pr1 X) _ _)). + apply iseqrelconstr. * intros x1 x2 x3 r1 r2. exact (r1 @ r2). * intro x. reflexivity. * intros x x' r. exact (!r). - apply make_isbinophrel; simpl; intros x1 x2 x3 r; rewrite r; reflexivity. Defined.