proposition: Lemma iscompbinoptransrel {X : setwithbinop} (R : hrel X) (ist : istrans R) (isb : isbinophrel R) : iscomprelrelfun2 R R (@op X).
proof: Proof. intros a b c d. intros rab rcd. set (racbc := pr2 isb a b c rab). set (rbcbd := pr1 isb c d b rcd). apply (ist _ _ _ racbc rbcbd). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions