i,j:
. no_repeats(;upto(i;j))l:T List, x:T. no_repeats(T;[x / l]) 
no_repeats(T;l) & 
(x 
l)i,j,k:. (k upto(i;j)) i
k & k < j| Rank | Theorem | Name |
| 3 | Thm* i,j:. no_repeats(;upto(i;j)) | [no_repeats_upto] |
| cites | ||
| 1 | Thm* l:T List, x:T. no_repeats(T;[x / l]) no_repeats(T;l) & (x l) | [no_repeats_cons] |
| 2 | Thm* i,j,k:. (k upto(i;j)) ik & k < j | [member_upto] |