'a:S, P:(eq('a)
Prop).
Thm* (
f:eq('a). P(f)) 
P(<eq_pred:(
x:'a. y:'a. x =
y)>)P:(('a'a
)Prop).
Thm* P(<eq_pred:(
x:'a. y:'a. x = y)>) (f:eq('a). P(f))is mentioned by
| 'a:S, P:(eq('a)Prop).
Thm* ( f:eq('a). P(f)) P(<eq_pred:(x:'a. y:'a. x = y)>) | [eq_pred_unabstraction] |
| P:(('a'a)Prop).
Thm* P(<eq_pred:( x:'a. y:'a. x = y)>) (f:eq('a). P(f)) | [eq_pred_abstraction] |
Try larger context:
HOLlib
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html