proposition: Lemma isapropissubsetwithbinop {X : hSet} (opp : binop X) (A : hsubtype X) : isaprop (issubsetwithbinop opp A).
proof: Proof. apply impred. intro a. apply impred. intros a'. apply (pr2 (A (opp (pr1 a) (pr1 a')))). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions