Def i == x:'a. x

is mentioned by

Thm* 'b,'a:S. all(f:'a  'b. and(equal(o(i,f),f),equal(o(f,i),f)))	[hi_o_id]
Thm* 'a:S. all(x:'a. equal(i(x),x))	[hi_thm]
Thm* 'a:S. equal(i,s(k,k))	[hi_def]

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