proposition: Lemma ispartbinophrelandfun {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 : @ispartbinophrel Y SY R) : @ispartbinophrel X SX (λ x x', R (f x) (f x')).
proof: Proof. set (ish := (pr2 f) : ∏ a0 b0, paths (f (op a0 b0)) (op (f a0) (f b0))). split. - intros a b c s r. rewrite (ish _ _). rewrite (ish _ _). apply ((pr1 is) _ _ _ (iss _ s) r). - intros a b c s r. rewrite (ish _ _). rewrite (ish _ _). apply ((pr2 is) _ _ _ (iss _ s) r). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions