Lemma iseqrel_generated_binopeqrel {X : setwithbinop} (R : hrel X) : iseqrel (generated_binopeqrel_hrel R). Proof. use iseqrelconstr. - intros x1 x2 x3 H1 H2 R' HR. eapply eqreltrans. + exact (H1 R' HR). + exact (H2 R' HR). - intros x R' HR. apply eqrelrefl. - intros x1 x2 H R' HR. apply eqrelsymm. exact (H R' HR). Defined.