Lemma isapropissubsetwith2binop {X : setwith2binop} (A : hsubtype X) : isaprop (issubsetwith2binop A). Proof. apply (isofhleveldirprod 1). - apply impred. intro a. apply impred. intros a'. apply (pr2 (A (op1 (pr1 a) (pr1 a')))). - apply impred. intro a. apply impred. intros a'. apply (pr2 (A (op2 (pr1 a) (pr1 a')))). Defined.