nil ; a.as1 f(a).mapc(f)(as1) (recursive)
A,B:Type, f:(A
B). mapc(f) 
(A List)(B List)| No mentions to report in SUPPORTjlc | |
| 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:
 |  |  |  |  |
 |  |  |  |  |  |