fact: Definition pr1subsetswith2binop (X : setwith2binop) : subsetswith2binop X -> hsubtype X := @pr1 _ (λ A : hsubtype X, issubsetwith2binop A).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions