Def eq('a) == {f:('a'a)| f = (x:'a. y:'a. x = y) }

is mentioned by

Thm* P  (f:eq('a). P)	[add_eq_pred_qf]
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* eq('a)  ('a'a)	[eq_pred_inc]

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