≝ λA,B.λf.∀x,y:A.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y → x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y.
definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
-≝λA,B.λf.∀z:B.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6x:A.z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
+≝λA,B.λf.∀z:B.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6x:A\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
≝ λA.λf.∀x,y.f x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y x.
lemma injective_compose : ∀A,B,C,f,g.
\ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A B f → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 B C g → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A C (λx.g (f x)).
-/3/; qed.
+/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/; qed.
(* extensional equality *)