proposition: Lemma trans_map_surjective : forall x y f, Transformation.surjective x y f = Map.surjective x y (Function.create x f).
proof: Proof. ir. ap iff_eq; ir. uhg; ee. wr trans_map_axioms. uh H; ee; am. uhg. ir. uh H; ee. uh H1. cp (H1 _ H0). nin H2. sh x1; ee. am. rw create_V_rewrite. am. am. uhg; ee. rw trans_map_axioms. uh H; ee; am. uhg; ir. uh H; ee. uh H1. cp (H1 _ H0). nin H2. sh x1; ee. am. rwi create_V_rewrite H3. am. am. Qed.
imports: set_theory