proposition: Lemma create_axioms : forall (p : E1) (x : E), axioms (create x p).
proof: Proof. ir. unfold axioms in |- *; xd. ir. ap pair_recov. unfold create in H. pose (Image.ex H). nin e. xd. rewrite <- H1. ap pair_is_pair. ir. unfold create in H. unfold create in H0. pose (Image.ex H). pose (Image.ex H0). nin e. nin e0. xd. rewrite <- H5. assert (x1 = x2). transitivity (pr1 x0). rewrite <- H5. sy; ap pr1_pair. rewrite H1. rewrite <- H4. ap pr1_pair. rewrite H6; am. Qed.
imports: set_theory