is mentioned by

Thm* 'a:S. equal(nil,abs_list(pair((n:hnum. select(e:'a. t)),0)))

[hnil_def]

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