Nuprl - Proof: eq pred unabstraction 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eq pred unabstraction 2 1

1. 'a : S
2. P : eq('a)

Prop
3. P(<eq_pred:(

x:'a.

y:'a. x =

y)>)
4. f : eq('a)

f = <eq_pred:(

x:'a.

y:'a. x =

y)>

By:

Analyze

Generated subgoals:

1 f = <eq_pred:(x:'a. y:'a. x = y)> 'a'a
2 steps

2 f = (x:'a. y:'a. x = y) 'a'a
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	f = <eq_pred:(x:'a. y:'a. x = y)> 'a'a	2 steps
2	f = (x:'a. y:'a. x = y) 'a'a	1 step