nil ; a.as1 [(f(a)) / (mapc(f)(as1))] (recursive)
A,B:Type, f:(A
B). mapc(f) 
(A List)(B List)| No other cites to report in MarkB_generic | |
| mapc | Def mapc(f)(as) == Case of as; nil nil ; a.as1 [(f(a)) / (mapc(f)(as1))] (recursive) |
| Thm* A,B:Type, f:(AB). mapc(f) (A List)(B List) |
About:
 |  |  |  |  |
 |  |  |  |  |  |