Lemma iscomprelrelfun_generated_binopeqrel {X Y : setwithbinop} {R : hrel X} {S : hrel Y} (f : binopfun X Y) (H : iscomprelrelfun R S f) : iscomprelrelfun (generated_binopeqrel R) (generated_binopeqrel S) f. Proof. intros x x' r. apply (r (pullback_binopeqrel f (generated_binopeqrel S))). intros x1 x2 r' S' s. use s. apply H. exact r'. Defined.