Definition isinvbinoptoispartinvbinop {X : setwithbinop} (S : hsubtype X) (L : hrel X) (d2 : isinvbinophrel L) : ispartinvbinophrel S L. Proof. unfold isinvbinophrel in d2. unfold ispartinvbinophrel. split. - intros a b c s. apply (pr1 d2 a b c). - intros a b c s. apply (pr2 d2 a b c). Defined.