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