fact: Definition binopeqrel_resp_left {X : setwithbinop} (R : binopeqrel X) {a b : X} (c : X) (r : R a b) : R (op c a) (op c b) := pr1 (pr2 R) a b c r.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions