proposition: Lemma mem_induction (C : V -> HProp) : (forall v, (forall x, x ∈ v -> C x) -> C v) -> forall v, C v.
proof: 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.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient