proposition: Lemma trans_map_injective : forall x y f, Transformation.injective x y f = Map.injective 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. rwi create_V_rewrite H2. rwi create_V_rewrite H2. uh H. ee. ap H3. am. am. am. am. am. uhg; ee. rw trans_map_axioms. uh H; ee; am. uhg; ir. uh H; ee. uh H3. cp (H3 _ _ H0 H1). ap H4. rw create_V_rewrite. rw create_V_rewrite. am. am. am. Qed.
imports: set_theory