f:(A
B), L:A List, P:(BProp). (x
map(f;L).P(x)) 
(xL.P(f(x)))a:T List, x:T', f:(TT'). (x map(f;a)) (
y:T. (y a) & x = f(y))| Rank | Theorem | Name |
| 3 | f:(AB), L:A List, P:(BProp). (xmap(f;L).P(x)) (xL.P(f(x))) | [l_all_map] |
| cites the following: | ||
| 2 | a:T List, x:T', f:(TT'). (x map(f;a)) (y:T. (y a) & x = f(y)) | [member_map] |