Def s == f:'a  'b  'c. g:'a  'b. x:'a. f(x,g(x))

is mentioned by

Thm* 'a,'b,'c:S. Thm* all Thm* (f:'a  'b  'c. all Thm* (f:'a  'b  'c. (g:'a  'b. all(x:'a. equal(s(f,g,x),f(x,g(x))))))	[hs_thm]
Thm* 'a:S. equal(i,s(k,k))	[hi_def]
Thm* 'c,'b,'a:S. equal(s,f:'a  'b  'c. g:'a  'b. x:'a. f(x,g(x)))	[hs_def]

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