proposition: Lemma isbinophrel_generated_binopeqrel {X : setwithbinop} (R : hrel X) : isbinophrel (generated_binopeqrel_hrel R).
proof: Proof. split. - intros a b c H R' H2. apply binopeqrel_resp_left. exact (H R' H2). - intros a b c H R' H2. apply binopeqrel_resp_right. exact (H R' H2). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions