proposition: Lemma injective_compose {X Y Z : Type} (f : X -> Y) (g : Y -> Z) : injective f -> injective g -> injective (compose g f).
proof: Proof. intros. red; intros. apply H0 in H1. apply H in H1. assumption. Qed.
imports: Coq(Description) Coq(FunctionalExtensionality)