s:(A+B) List. no_repeats(A+B;s) 
no_repeats(A;mapoutl(s))l:T List, x:T. no_repeats(T;[x / l]) 
no_repeats(T;l) & 
(x 
l)s:(A+B) List, x:A. (x mapoutl(s)) (
y:A+B. (y s) & isl(y) & x = outl(y))| Rank | Theorem | Name |
| 4 | Thm* s:(A+B) List. no_repeats(A+B;s) no_repeats(A;mapoutl(s)) | [no_repeats_mapoutl] |
| cites | ||
| 1 | Thm* l:T List, x:T. no_repeats(T;[x / l]) no_repeats(T;l) & (x l) | [no_repeats_cons] |
| 3 | Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y)) | [member_mapoutl] |