a:T List, x:T', f:(T
T'). (x 
map(f;a)) 
(
y:T. (y a) & x = f(y))f:(AB), as:A List. ||map(f;as)|| = ||as|| 
f:(AB), as:A List, n:
||as||. map(f;as)[n] = f(as[n])| Rank | Theorem | Name |
| 2 | a:T List, x:T', f:(TT'). (x map(f;a)) (y:T. (y a) & x = f(y)) | [member_map] |
| cites the following: | ||
| 0 | f:(AB), as:A List. ||map(f;as)|| = ||as|| | [map_length] |
| 1 | f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n]) | [map_select] |