a:T List, f:(T
T). (x:T. (x 
a) 
f(x) = x) map(f;a) = aa:T List, f,g:(TT').
Thm* (
x:T. (x a) f(x) = g(x)) map(f;a) = map(g;a)as:A List. map(Id;as) = as| Rank | Theorem | Name |
| 4 | a:T List, f:(TT). (x:T. (x a) f(x) = x) map(f;a) = a | [trivial_map] |
| cites the following: | ||
| 3 | a:T List, f,g:(TT').
Thm* ( x:T. (x a) f(x) = g(x)) map(f;a) = map(g;a) | [map_equal2] |
| 0 | as:A List. map(Id;as) = as | [map_id] |