proposition: Lemma restr_domain : forall f x, Function.axioms f -> domain (restr f x) = intersection2 (domain f) x.
proof: Proof. ir. ap extensionality; uhg; ir. ufi domain H0. rwi Image.inc_rw H0. nin H0; ee. ufi restr H0; Ztac. ap intersection2_inc. uf domain. rw Image.inc_rw. sh x1; ee. am. am. wr H1; am. cp (intersection2_first H0). cp (intersection2_second H0). uf domain. rw Image.inc_rw. ufi domain H1. rwi Image.inc_rw H1. nin H1; ee. sh x1. ee; try am. uf restr; ap Z_inc. am. rw H3; am. Qed.
imports: set_theory