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]
8. (a:A. i:(k-1). f(i)  a)
  n:. A ~ n

By:	FwdThru: Thm*  (x:T. Q(x))  (x:T. Q(x)) on [ Hyp:-1 ] THEN Witness: k-1

1

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

6 steps

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