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

1

6. n :  7. A ~ n 8. k:. f:(kA). i,j:k. i<j  R(f(i);f(j))   x:A. R(x;x)

14 steps

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