a:T List, f,g:(T
T').
Thm* (
x:T. (x 
a) 
f(x) = g(x)) map(f;a) = map(g;a)a:T List, f,g:(TT').
Thm* (
i:
. i<||a|| f(a[i]) = g(a[i])) map(f;a) = map(g;a)| Rank | Theorem | Name |
| 3 | a:T List, f,g:(TT').
Thm* ( x:T. (x a) f(x) = g(x)) map(f;a) = map(g;a) | [map_equal2] |
| cites the following: | ||
| 2 | a:T List, f,g:(TT').
Thm* ( i:. i<||a|| f(a[i]) = g(a[i])) map(f;a) = map(g;a) | [map_equal] |