Def x = y == (x = y  T)

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* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a). Thm* iso_pair('a;'b;P;rep;abs) Thm*  Thm* (a:'a. abs(rep(a)) = a) & (r:'b. P(r) = ((rep(abs(r))) = r))	[iso_pair_char]
Thm* x,y:. (x = y)  (x  y)	[assert_of_bequal_bools]
Thm* x,y:T. (x = y)  x = y	[assert_of_bequal]
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