Definition pullback_binopeqrel_rev {X Y : setwithbinop} (f : binopfun X (setwithbinop_rev Y)) (R : binopeqrel Y) : binopeqrel X. Proof. apply (pullback_binopeqrel f). use make_binopeqrel. - exact R. - apply make_isbinophrel; intros x1 x2 x3 r; apply (pr2 R); exact r. Defined.