r:
, k:
, L: List. r- > L^k 
Propf:(A
B), as:A List, n:||as||. map(f;as)[n] = f(as[n])f:(AB), as:A List. ||map(f;as)|| = ||as|| k:, f:(k). increasing(f;k) 
(x,y:k. x < y f(x) < f(y))| Rank | Theorem | Name |
| 2 | Thm* r:, k:, L: List. r- > L^k Prop | [arrows_wf] |
| cites | ||
| 1 | Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n]) | [map_select] |
| 0 | Thm* f:(AB), as:A List. ||map(f;as)|| = ||as|| | [map_length] |
| 0 | Thm* k:, f:(k). increasing(f;k) (x,y:k. x < y f(x) < f(y)) | [increasing_implies] |