-lemma injective_compose : ∀A,B,C,f,g.
-injective A B f → injective B C g → injective A C (λx.g (f x)).
-/3/; qed.
+\ 5img class="anchor" src="icons/tick.png" id="injective_compose"\ 6lemma 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)).
+/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/; qed.