Require Import Coq.Sets.Image.

Theorem injective_trans:
forall A B C (f: A -> B) (g:B -> C) (h:A -> C),
(forall x, h x = g (f x)) -> injective A B f -> injective B C g -> injective A C h.
Proof.
intros A B C f g h H_h_equal_g_f H_f_injective H_g_injective.
unfold injective in *.
intros x y H_h_x_y.
apply H_f_injective.
apply H_g_injective.
rewrite <- H_h_equal_g_f.
rewrite <- H_h_equal_g_f.
apply H_h_x_y.
Qed.