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