'a:S. iso_pair('a List;(
'a)
;is_list_rep;rep_list;abs_list)as:T List. (
i:||as||. as[i]){||as||} = asm,n:
, f:({m..n
}T). n<m 
||f{m..n}|| = n-m 
n:, f:(nT), i:n. (f{n})[i] = f(i)'a:S. equal(arb,select(x:'a. t))| Rank | Theorem | Name |
| 7 | 'a:S. iso_pair('a List;('a);is_list_rep;rep_list;abs_list) | [list_iso] |
| cites the following: | ||
| 1 | as:T List. (i:||as||. as[i]){||as||} = as | [listify_select_id] |
| 6 | m,n:, f:({m..n}T). n<m ||f{m..n}|| = n-m | [listify_length] |
| 6 | n:, f:(nT), i:n. (f{n})[i] = f(i) | [select_listify_id] |
| 1 | 'a:S. equal(arb,select(x:'a. t)) | [harb_wd] |