proposition: Lemma create_inc : forall (x y : E) (hyp : inc y x) (p : E1) (z : E), pair y (p y) = z -> inc z (create x p).
proof: Proof. ir. unfold create in |- *. ap Image.show_inc. apply ex_intro with y; xd. Qed.
imports: set_theory