Who Cites hmap?
hmap	Def map == f:'a'b. l:'a List. map(f;l)
	Thm* 'a,'b:S. map  (('a  'b)  hlist('a)  hlist('b))
map	Def map(f;as) == Case of as; nil  nil ; a.as'  cons((f(a)); map(f;as')) Def (recursive)
	Thm* A,B:Type, f:(AB), l:A List. map(f;l)  B List
tlambda	Def (x:T. b(x))(x) == b(x)

Syntax:

map

has structure:

hmap('a; 'b)

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html