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