nil ; a.as' [(f(a,as')) / mapcons(f;as')] (recursive)
A,B:Type, f:(A
(A List)B), l:A List. mapcons(f;l) 
B List| Who Cites mapcons? | |
| mapcons | Def mapcons(f;as) == Case of as; nil nil ; a.as' [(f(a,as')) / mapcons(f;as')] (recursive) |
| Thm* A,B:Type, f:(A(A List)B), l:A List. mapcons(f;l) B List |
| Syntax: | mapcons(f;as) | has structure: | mapcons(f; as) |
About:
 |  |  |  |  |
 |  |  |  |  |  |