1. k : 
2. 0<k
3. p:((k-1)(k-1)). 
3. Bij((k-1); (k-1); p)  (L:(k-1-1) List. p = compose_flips(L))
4. p : kk
5. Bij(k; k; p)
  x:k. p(x) = k-1

1

5. Inj(k; k; p) 6. b:k. a:k. p(a) = b   x:k. p(x) = k-1

2 steps

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