proposition: Lemma create_V_out : forall x f y, ~inc y x -> V y (create x f) = emptyset.
proof: Proof. ir. cp (V_or y (create x f)). nin H0. assert (axioms (create x f)). app create_axioms. cp (lem2 H1 H0). rwi pr1_pair H2. rwi create_domain H2. nin (H H2). ee; am. Qed.
imports: set_theory