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] |