Lemma binophrelandfun {X Y : setwithbinop} (f : binopfun X Y) (R : hrel Y) (is : @isbinophrel Y R) : @isbinophrel X (λ x x', R (f x) (f x')). Proof. set (ish := (pr2 f) : ∏ a0 b0, f (op a0 b0) = op (f a0) (f b0)). split. - intros a b c r. rewrite (ish _ _). rewrite (ish _ _). apply (pr1 is). apply r. - intros a b c r. rewrite (ish _ _). rewrite (ish _ _). apply (pr2 is). apply r. Defined.