fact: Definition generated_binophrel {X : setwithbinop} (R : hrel X) : binophrel X := make_binophrel (generated_binophrel_hrel R) (isbinophrel_generated_binophrel R).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions