proposition: Lemma compose_injective : forall x y z f g, Transformation.injective x y f -> Transformation.injective y z g -> Transformation.injective x z (fun y=> g (f y)).
proof: Proof. ir. uhg; dj. apply Transformation.compose_axioms with y. lu. lu. uhg; ir. uh H; uh H0. ee. assert (f x0 = f y0). ap H5. ap H. am. ap H; am. am. ap H6. am. am. am. Qed.
imports: set_theory