proposition: Lemma isapropissubsetwith2binop {X : setwith2binop} (A : hsubtype X) : isaprop (issubsetwith2binop A).
proof: 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.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions