Nuprl - Proof: bijection restriction 2 1

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

1. k :

2. f :

k
3. 0<k
4.

a1,a2:

k. f(a1) = f(a2)

a1 = a2
5. f(k-1) = k-1
6. f

(k-1)

(k-1)
7. a1 :

(k-1)
8.

a2:

k. f(a1) = f(a2)

a1 = a2
9. a2 :

(k-1)
10. f(a1) = f(a2)

a1 = a2
11. f(a1) = f(a2)

a1 = a2

By:	Analyze -2

Generated subgoals:

None

About:

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