is mentioned by

Thm* s:(A+B) List. no_repeats(A+B;s) no_repeats(A;mapoutl(s))	[no_repeats_mapoutl]
Thm* i,j:. no_repeats(;upto(i;j))	[no_repeats_upto]
Thm* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) (x:T. (x A) & (x B)) ||A|| < ||B||	[length_less]
Thm* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) ||A||||B||	[length_le]
Thm* L:T List. no_repeats(T;rev(L)) no_repeats(T;L)	[no_repeats_reverse]
Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2)	[no_repeats_append_iff]
Thm* t:T. no_repeats(T;[t])	[no_repeats_singleton]
Thm* s:T List. no_repeats(T;s) (f:(||s||T). Inj(||s||; T; f))	[no_repeats_inj]

In prior sections: mb list 2

Try larger context: Graphs