Theorem setquotunivprop' {X : UU} {R : eqrel X} (P : setquot (pr1 R) -> UU) (H : ∏ x, isaprop (P x)) (ps : ∏ x : X, P (setquotpr R x)) : ∏ c : setquot (pr1 R), P c. Proof. exact (setquotunivprop R (λ x, make_hProp (P x) (H x)) ps). Defined.