proposition: Lemma create_V_apply : forall (x : E) (p : E1) (y z : E), inc y x -> p y = z -> V y (create x p) = z.
proof: Proof. ir. assert (inc (pair y (V y (create x p))) (create x p)). ap V_inc. apply ex_intro with (p y). ap (create_inc H). tv. tv. assert (axioms (create x p)). ap create_axioms. unfold axioms in H2; xd. assert (pair y (V y (create x p)) = pair y z). ap H3. ap V_inc. apply ex_intro with (p y). ap (create_inc H). tv. tv. ap (create_inc H). rewrite H0; tv. rewrite pr1_pair. rewrite pr1_pair. tv. transitivity (pr2 (pair y z)). rewrite <- H4. sy; ap pr2_pair. ap pr2_pair. Qed.
imports: set_theory