Def map2 == f:'a'b. l1:'a. l2:'b. map2(f;l1;l2)

is mentioned by

Thm* 'a,'b,'c:S. Thm* and Thm* (all(f:'a  'b  'c. equal(map2(f,nil,nil),nil)) Thm* ,all Thm* ,(f:'a Thm* ,( 'b Thm* ,( 'c. all Thm* ,( 'c. (h1:'a. all Thm* ,( 'c. (h1:'a. (t1:hlist Thm* ,( 'c. (h1:'a. (('a). all Thm* ,( 'c. (h1:'a. (('a). (h2:'b. all Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). equal Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (map2 Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ((f Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (,cons(h1,t1) Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (,cons(h2,t2)) Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,cons Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,(f(h1,h2) Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,,map2(f,t1,t2)))))))))

[hmap2_wd]

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