1. P:Prop. P  P
2. A : Type
3. (n:. A ~ n)
4. k : 
5. 0<k
6. f : (k-1)A
7. Inj((k-1); A; f)  [not for witness]
  (a:A. i:(k-1). f(i)  a)

1

8. (a:A. i:(k-1). f(i)  a)   n:. A ~ n

7 steps

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