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