Nuprl - Proof: bijection restriction 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bijection restriction 1 1

1. k :

2. f :

k
3. 0<k
4. Bij(

k; f)
5. f(k-1) = k-1
6. z :

(k-1)

f(z)

(k-1)

By:	Decide (f(z) = k-1)

Generated subgoal:

1 7. f(z) = k-1
f(z) (k-1)
1 step

About:

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