1. A : Type
2. k : 
3. k1:. 
3. k1<k
3. 
3. (Q:(k1AProp). 
3. ((x:k1. y:A. Q(x;y))  (f:(k1A). x:k1. Q(x;f(x))))
4. Q : kAProp
5. x:k. y:A. Q(x;y)
6. k = 0
7. g : (k-1)A
8. x:(k-1). Q(x;g(x))
9. y : A
10. Q(k-1;y)
  f:(kA). f(k-1) = y & (x:(k-1). f(x) = g(x))

By:	Witness: x.if x=k-1 y else g(x) fi with type kA THENP (Analyze THEN SplitITE Concl)

1

11. (x.if x=k-1 y else g(x) fi)  kA   if k-1=k-1 y else g(k-1) fi = y   & (x:(k-1). if x=k-1 y else g(x) fi = g(x))

1 step

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