is mentioned by

Thm* k1,k2:. f:((k1+k2)(k1+k2)). Inj(k1+k2; (k1+k2); f)	[union_cardinality1]
Thm* f:(AB), g:(BC). Inj(A; B; f) Inj(B; C; g) Inj(A; C; g o f)	[compose_inject]
Thm* s:T List. no_repeats(T;s) (f:(||s||T). Inj(||s||; T; f))	[no_repeats_inj]

In prior sections: mb nat fun 1

Try larger context: Graphs