f:(T
T'), x,y:T, s:T List. x before y 
s 
f(x) before f(y) map(f;s)f:(AB), as:A List, n:
||as||. map(f;as)[n] = f(as[n])| Rank | Theorem | Name |
| 2 | Thm* f:(TT'), x,y:T, s:T List. x before y s f(x) before f(y) map(f;s) | [map_before] |
| cites | ||
| 1 | Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n]) | [map_select] |