\forall g: B\to B\to B. Prop
\def \lambda A,B.\lambda f,g.\forall x:A.\forall y,z:B. f x (g y z) = g (f x y) (f x z).
+lemma injective_compose : ∀A,B,C,f,g.injective A B f → injective B C g →
+ injective A C (λx.g (f x)).
+intros;unfold;intros;simplify in H2;apply H;apply H1;assumption;
+qed.
\ No newline at end of file