proposition: Lemma isbinopreflrel {X : setwithbinop} (R : hrel X) (isr : isrefl R) (isb : iscomprelrelfun2 R R (@op X)) : isbinophrel R.
proof: 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.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions