proposition: Lemma domain_union : forall z:E, domain (union z) = union (Image.create z domain).
proof: Proof. ir. ap extensionality; uhg; ir. ufi domain H. rwi Image.inc_rw H. nin H. ee. nin (union_exists H). ee. apply union_inc with (domain x1). uf domain; rw Image.inc_rw. sh x0; xd. rw Image.inc_rw. sh x1; xd. nin (union_exists H). ee. rwi Image.inc_rw H1. nin H1; ee. uf domain; rw Image.inc_rw. ufi domain H2. wri H2 H0. rwi Image.inc_rw H0. nin H0; ee. sh x2; xd. apply union_inc with x1. am. am. Qed.
imports: set_theory