A,B:T List. no_repeats(T;A) 
(x:T. (x 
A) (x B)) (
x:T. 
(x A) & (x B)) ||A|| < ||B||k,m:
. (f:(k
m). Inj(k; m; f)) k
m| Rank | Theorem | Name |
| 2 | 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] |
| cites | ||
| 1 | Thm* k,m:. (f:(km). Inj(k; m; f)) km | [injection_le] |