1. k : 
2. k1:. 
2. k1<k
2. 
2. (B:(k1Type), Q:(x:k1B(x)Prop).
2. ((x:k1. y:B(x). Q(x;y))  (f:(x:k1B(x)). x:k1. Q(x;f(x))))
3. B : kType
4. Q : x:kB(x)Prop
5. x:k. y:B(x). Q(x;y)
6. k = 0
7. g : x:(k-1)B(x)
8. x:(k-1). Q(x;g(x))
9. y : B(k-1)
10. Q(k-1;y)
11. f : x:kB(x)
12. f(k-1) = y
13. x:(k-1). f(x) = g(x)
14. x : k
  Q(x;f(x))

By:	Decide: x = k-1  k

1	15. x = k-1  k   Q(x;f(x))	6 steps
2	15. x = k-1  k   Q(x;f(x))	3 steps

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