proposition: Lemma create_V_defined : forall (x : E) (p : E1) (y : E), defined (create x p) y -> V y (create x p) = p y.
proof: Proof. ir. ap create_V_apply. unfold defined in H. xd. rewrite create_domain in H0. am. tv. Qed.
imports: set_theory