Rank | Theorem | Name |
2 | Thm* a:T List, f,g:(T T').
Thm* ( i: . i<||a||  f(a[i]) = g(a[i]))  map(f;a) = map(g;a) | [map_equal] |
cites the following: |
1 | Thm* a,b:T List. ||a|| = ||b||  ( i: . i<||a||  a[i] = b[i])  a = b | [list_extensionality] |
1 | Thm* f:(A B), as:A List, n: ||as||. map(f;as)[n] = f(as[n]) | [map_select] |
0 | Thm* f:(A B), as:A List. ||map(f;as)|| = ||as||  | [map_length] |