proposition: Lemma create_domain : forall (x : E) (p : E1), domain (create x p) = x.
proof: Proof. ir. unfold domain in |- *. ap extensionality; unfold sub in |- *; ir. pose (Image.ex H); nin e; xd. unfold create in H0; pose (Image.ex H0); nin e; xd. rewrite <- H1. assert (pr1 x1 = x2). rewrite <- H3; ap pr1_pair. rewrite H4; au. ap Image.show_inc. apply ex_intro with (pair x0 (p x0)). xd. ap (create_inc H); au. ap pr1_pair. Qed.
imports: set_theory