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