forall x, ~ (x ∈ V_empty). Proof. intros x Hx. generalize Hx; apply Trunc_rec. intros [ff _]. exact ff. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.