Definition generated_binopeqrel {X : setwithbinop} (R : hrel X) : binopeqrel X := make_binopeqrel (make_eqrel (generated_binopeqrel_hrel R) (iseqrel_generated_binopeqrel R)) (isbinophrel_generated_binopeqrel R).