\lambda A,B,C:Type.\lambda f:(B\to C).\lambda g:(A\to B).\lambda x:A.
f (g x).
-notation "hvbox(a break \circ b)"
- left associative with precedence 70
-for @{ 'compose $a $b }.
-
-interpretation "function composition" 'compose f g =
- (cic:/matita/higher_order_defs/functions/compose.con _ _ _ f g).
+interpretation "function composition" 'compose f g = (compose ? ? ? f g).
definition injective: \forall A,B:Type.\forall f:A \to B.Prop
\def \lambda A,B.\lambda f.
\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