A,B:T List. no_repeats(T;A) 
(x:T. (x 
A) (x B)) ||A||
||B||k,m:
. (
f:(k
m). Inj(k; m; f)) km| Rank | Theorem | Name |
| 2 | Thm* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) ||A||||B|| | [length_le] |
| cites | ||
| 1 | Thm* k,m:. (f:(km). Inj(k; m; f)) km | [injection_le] |