fact: Definition pr1subsetswithbinop (X : setwithbinop) : subsetswithbinop X -> hsubtype X := @pr1 _ (λ A : hsubtype X, issubsetwithbinop (@op X) A).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions