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