Def map == f:'a'b. l:'a List. map(f;l)

is mentioned by

Thm* 'b,'a:S. Thm* all(l:hlist('a). all(f:'a  'b. equal(length(map(f,l)),length(l))))	[hlength_map]
Thm* 'a,'b:S. Thm* all Thm* (f:'a  'b. all Thm* (f:'a  'b. (l1:hlist('a). all Thm* (f:'a  'b. (l1:hlist('a). (l2:hlist('a). equal Thm* (f:'a  'b. (l1:hlist('a). (l2:hlist('a). (map(f,append(l1,l2)) Thm* (f:'a  'b. (l1:hlist('a). (l2:hlist('a). ,append Thm* (f:'a  'b. (l1:hlist('a). (l2:hlist('a). ,(map(f,l1) Thm* (f:'a  'b. (l1:hlist('a). (l2:hlist('a). ,,map(f,l2))))))	[hmap_append_2]
Thm* 'a,'b:S. Thm* and Thm* (all(f:'a  'b. equal(map(f,nil),nil)) Thm* ,all Thm* ,(f:'a  'b. all Thm* ,(f:'a  'b. (h:'a. all Thm* ,(f:'a  'b. (h:'a. (t:hlist('a). equal Thm* ,(f:'a  'b. (h:'a. (t:hlist('a). (map(f,cons(h,t)) Thm* ,(f:'a  'b. (h:'a. (t:hlist('a). ,cons(f(h),map(f,t)))))))	[hmap_wd]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html