proposition: Lemma trans_sub_bijective : forall x y f u, Transformation.injective x y f -> sub u x -> Transformation.bijective u (Image.create u f) f.
proof: Proof. ir. uhg; dj. uhg; ee. ir. rw Image.inc_rw. sh x0; ee; try tv. uhg; ee; try am. uhg. ir. rwi Image.inc_rw H2. nin H2; ee. sh x1; ee; am. uhg; ee; try am. uhg; ir. uh H; ee. uh H6; ee. ap H6; try am. ap H0; am. ap H0; am. Qed.
imports: set_theory