proposition: Lemma generated_binophrel_intro {X : setwithbinop} {R : hrel X} {x x' : X} (r : R x x') : generated_binophrel R x x'.
proof: Proof. intros R' H. exact (H x x' r). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions