Def k == x:'a. y:'b. x

is mentioned by

Thm* 'a,'b:S. all(x:'a. all(y:'b. equal(k(x,y),x)))	[hk_thm]
Thm* 'a:S. equal(i,s(k,k))	[hi_def]
Thm* 'a,'b:S. equal(k,x:'a. y:'b. x)	[hk_def]

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