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. n : 
7. A ~ n
8. k:. f:(kA). i,j:k. i<j  R(f(i);f(j))
  x:A. R(x;x)

1

9. f : (n+1)A 10. i,j:(n+1). i<j  R(f(i);f(j))   x:A. R(x;x)

13 steps

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