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. e : An
8. g : nA
9. InvFuns(A;n;e;g)
10. k:. f:(kA). i,j:k. i<j  R(f(i);f(j))
11. f : (n+1)A
12. i,j:(n+1). i<j  R(f(i);f(j))
13. x,y:(n+1). x  y & (e o f)(x) = (e o f)(y)
14. x : (n+1)
15. y : (n+1)
16. x<y
17. (e o f)(x) = (e o f)(y)
  x:A. R(x;x)

1

18. x:A. g(e(x)) = x  A   x:A. R(x;x)

5 steps

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