Lemma isbinopreflrel {X : setwithbinop} (R : hrel X) (isr : isrefl R) (isb : iscomprelrelfun2 R R (@op X)) : isbinophrel R. Proof. split. - intros a b c rab. apply (isb c c a b (isr c) rab). - intros a b c rab. apply (isb a b c c rab (isr c)). Defined.