proposition: Theorem isasetsetquot {X : UU} (R : hrel X) : isaset (setquot R).
proof: Proof. apply (isasetsubset (@pr1 _ _) (isasethsubtype X)). apply isinclpr1; intro x. apply isapropiseqclass. Defined.
imports: UniMath.Foundations.Propositions