Theorem setquotuniv4prop {X : UU} (R : eqrel X) (P : setquot R -> setquot R -> setquot R -> setquot R -> hProp) (is : ∏ x x' x'' x''' : X, P (setquotpr R x) (setquotpr R x') (setquotpr R x'') (setquotpr R x''')) : ∏ c c' c'' c''' : setquot R, P c c' c'' c'''. Proof. intros. assert (int1 : ∏ c0 c0' c0'' : _, P c c0 c0' c0''). { apply (setquotuniv3prop R (λ c0 c0' c0'', P c c0 c0' c0'')). intros x x' x''. apply (setquotunivprop R (λ c0 : _, P c0 (setquotpr R x) (setquotpr R x') (setquotpr R x''))). intro x0. apply (is x0 x x' x''). } apply (int1 c' c'' c'''). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.