(C : V -> HProp) : (forall v, (forall x, x ∈ v -> C x) -> C v) -> forall v, C v. Proof. intro H. refine (V_ind_hprop _ _ _). intros A f H_f. apply H. intros x Hx. generalize Hx; apply Trunc_rec. intros [a p]. exact (transport C p (H_f a)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.