proposition: Lemma elt_rewrite : forall (x : E) (p : E1) (y : E), inc y (create x p) -> y = pair (pr1 y) (p (pr1 y)).
proof: Proof. ir. unfold create in H. pose (Image.ex H). nin e. xd. assert (pr1 y = x0). rewrite <- H1. ap pr1_pair. rewrite H2. au. Qed.
imports: set_theory