Def select == p:'a. @x:'a. (p(x))

is mentioned by

Thm* equal(zero_rep,select(x:hind. all(y:hind. not(equal(x,suc_rep(y))))))	[hzero_rep_def]
Thm* equal(suc_rep,select(f:hind  hind. and(one_one(f),not(onto(f)))))	[hsuc_rep_def]

In prior sections: hol bool

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