IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq pred unabstraction1 1. 'a : S
2. P : eq('a)Prop
3. f:eq('a). P(f)
P(<eq_pred:(x:'a. y:'a. x =y)>)
By:
BackThru 3 THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
f:eq('a). P(f)
P(<eq_pred:(
x:'a. 
y)>)
