PrintForm Definitions hol list 2 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hmap2 wd
  'a,'b,'c:S.
  and
  (all(f:'a  'b  'c. equal(map2(f,nil,nil),nil))
  ,all
  ,(f:'a
  ,( 'b
  ,( 'c. all
  ,( 'c. (h1:'a. all
  ,( 'c. (h1:'a. (t1:hlist
  ,( 'c. (h1:'a. (('a). all
  ,( 'c. (h1:'a. (('a). (h2:'b. all
  ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). equal
  ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (map2
  ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ((f
  ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (,cons(h1,t1)
  ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (,cons(h2,t2))
  ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,cons
  ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,(f(h1,h2)
  ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,,map2(f,t1,t2)))))))))
By: HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

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

PrintForm Definitions hol list 2 Sections HOLlib Doc