1. A : Type
2. R : AAProp
3. A
4. Trans x,y:A. R(x;y)
5. x:A. y:A. R(x;y)
6. k : 
  f:(kA). i,j:k. i<j  R(f(i);f(j))

1	6. k :  7. 0<k 8. 1 = k   f:(kA). i,j:k. i<j  R(f(i);f(j))	1 step
2	6. k :  7. 1<k 8. f:((k-1)A). i,j:(k-1). i<j  R(f(i);f(j))   f:(kA). i,j:k. i<j  R(f(i);f(j))	11 steps

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