Lemma iscomprelfun_generated_binopeqrel {X Y : setwithbinop} {R : hrel X} (f : binopfun X Y) (H : iscomprelfun R f) : iscomprelfun (generated_binopeqrel R) f. Proof. intros x x' r. exact (r (binopeqrel_of_binopfun f) H). Defined.