Lemma ispartbinophrelif {X : setwithbinop} (S : hsubtype X) (R : hrel X) (is : iscomm (@op X)) (isl : ∏ a b c : X, S c → R a b → R (op c a) (op c b)) : ispartbinophrel S R. Proof. exists isl. intros a b c s rab. induction (is c a). induction (is c b). apply (isl _ _ _ s rab). Defined.