Def add == m:. n:. m+n

is mentioned by

Thm* 'a:S.  Thm* all Thm* (l1:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). equal Thm* (l1:hlist('a). (l2:hlist('a). (length(append(l1,l2)) Thm* (l1:hlist('a). (l2:hlist('a). ,add(length(l1),length(l2)))))	[hlength_append_2]
Thm* and Thm* (equal(it_sum(nil),0) Thm* ,all Thm* ,(h:hnum. all(t:hlist(hnum). equal(it_sum(cons(h,t)),add(h,it_sum(t))))))	[hit_sum_wd]

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