'b,'a:S, l:'a List, f:('a
'b). ||map(f;l)|| = ||l|| 
'b,'a:S.
Thm* all(
l:hlist('a). all(f:'a 'b. equal(length(map(f,l)),length(l))))| Theorem | Name |
| 'b,'a:S, l:'a List, f:('a'b). ||map(f;l)|| = ||l|| | [length_map] |
| cites the following: | |
| 'b,'a:S.
Thm* all( l:hlist('a). all(f:'a 'b. equal(length(map(f,l)),length(l)))) | [hlength_map] |