proposition: Lemma iscomprelfun_generated_binopeqrel {X Y : setwithbinop} {R : hrel X} (f : binopfun X Y) (H : iscomprelfun R f) : iscomprelfun (generated_binopeqrel R) f.
proof: Proof. intros x x' r. exact (r (binopeqrel_of_binopfun f) H). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions