IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq pred unabstraction212 1. 'a : S
2. P : eq('a)Prop
3. P(<eq_pred:(x:'a. y:'a. x =y)>)
4. f : eq('a)
f = (x:'a. y:'a. x =y) 'a'a
By:
Analyze 4 THEN StrongAuto THEN Try (Complete (Unfold `label` 0))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
x:'a. 
y)>)
f = (
'a
