Nuprl - Proof: nsub bij ooc invpair 1 1 1 1

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

1. a :

2. f :

a bij

<f,

y.least x:

. f(x)=

(

By:	f a bij a Asserted THEN Analyze-1

Generated subgoal:

1 3. f aa
4. Bij(a; a; f)
<f,y.least x:. f(x)=y> (aa)(aa)
2 steps

About:

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