Nuprl - Proof: nsub bij ooc invpair 1 3 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub bij ooc invpair 1 3 1

1. a :

2. (

f.<f,

y.least x:

. f(x)=

y>)

(

a bij

a
3. (

fg.fg/f,g. f)

(

a bij

x:(

a bij

a). (

fg.fg/f,g. f)((

f.<f,

y.least x:

. f(x)=

y>)(x)) = x

By:	New:f Analyze

Generated subgoal:

1 4. f : a bij a
(fg.fg/f,g. f)((f.<f,y.least x:. f(x)=y>)(f)) = f
1 step

About:

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