IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq pred abstraction1 1. 'a : Type
2. P : ('a'a)Prop
3. P(x:'a. y:'a. x =y)
4. f : eq('a)
P(f)
By:
RW (TopC (LemmaC Thm*f:eq('a). f = (x:'a. y:'a. x =y) 'a'a)) 0
THEN
StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'a
)
x:'a. 
y)
P(f)
f:eq('a). f = (
'a
