Lemma isbinophrel_generated_binopeqrel {X : setwithbinop} (R : hrel X) : isbinophrel (generated_binopeqrel_hrel R). 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.