1. k : 
2. f : kk
3. 0<k
4. Bij(k; k; f)
5. f(k-1) = k-1
6. f  (k-1)(k-1)
  Bij((k-1); (k-1); f)

1

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)  k  a1 = a2  k 9. a2 : (k-1) 10. f(a1) = f(a2)  k  a1 = a2  k 11. f(a1) = f(a2)   a1 = a2

1 step

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