Lemma isapropissubsetwithbinop {X : hSet} (opp : binop X) (A : hsubtype X) : isaprop (issubsetwithbinop opp A). Proof. apply impred. intro a. apply impred. intros a'. apply (pr2 (A (opp (pr1 a) (pr1 a')))). Defined.