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