Lemma ispartinvbinophrelandfun {X Y : setwithbinop} (f : binopfun X Y) (SX : hsubtype X) (SY : hsubtype Y) (iss : ∏ x : X, (SX x) → (SY (f x))) (R : hrel Y) (is : @ispartinvbinophrel Y SY R) : @ispartinvbinophrel X SX (λ 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 s r. rewrite (ish _ _) in r. rewrite (ish _ _) in r. apply ((pr1 is) _ _ _ (iss _ s) r). - intros a b c s r. rewrite (ish _ _) in r. rewrite (ish _ _) in r. apply ((pr2 is) _ _ _ (iss _ s) r). Defined.