Def (x:T. b(x))(x) == b(x)

is mentioned by

Thm* 'a:S, P:(eq('a)Prop). Thm* (f:eq('a). P(f))  P(<eq_pred:(x:'a. y:'a. x = y)>)	[eq_pred_unabstraction]
Thm* P:(('a'a)Prop).  Thm* P(<eq_pred:(x:'a. y:'a. x = y)>)  (f:eq('a). P(f))	[eq_pred_abstraction]
Thm* 'a:S. <eq_pred:(x:'a. y:'a. x = y)>  eq('a)	[eq_pred_marker_wf]
Thm* f:eq('a). f = (x:'a. y:'a. x = y)  'a'a	[eq_pred_char]
Thm* 'a,'b:S. Thm* (p:'a'b. a:'a. b:'b. (a = 1of(p))(b = 2of(p))) Thm* = Thm* (@rep:'a'b'a'b Thm* (@((p',p'':'a'b.  ((rep(p')) = (rep(p'')))(p' = p'')) Thm* (@(x:'a'b Thm* (@(((his_pair('a; 'b)(x)) = (p':'a'b. (x = (rep(p'))))))))	[rep_prod_axiom]
Thm* f,g:('a'b). f = (x:'a. g(x))  (x:'a. f(x) = g(x))	[ext_simp_2]
Thm* f,g:('a'b). (x:'a. f(x)) = (x:'a. g(x))  (x:'a. f(x) = g(x))	[ext_simp_1]
Def eq('a) == {f:('a'a)| f = (x:'a. y:'a. x = y) }	[eq_pred]

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