Theorem setquotuniv2prop' {X : UU} {R : eqrel X} (P : setquot (pr1 R) → setquot (pr1 R) → UU) (H : ∏ x1 x2, isaprop (P x1 x2)) (ps : ∏ x1 x2, P (setquotpr R x1) (setquotpr R x2)) : ∏ c1 c2 : setquot (pr1 R), P c1 c2. Proof. exact (setquotuniv2prop R (λ x1 x2, make_hProp (P x1 x2) (H x1 x2)) ps). Defined.