proposition: Lemma isbinophrelif {X : setwithbinop} (R : hrel X) (is : iscomm (@op X)) (isl : ∏ a b c : X, R a b -> R (op c a) (op c b)) : isbinophrel R.
proof: Proof. split with isl. intros a b c rab. destruct (is c a). destruct (is c b). apply (isl _ _ _ rab). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions