fact: 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).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions