A:Type, R:(AAProp).
  (A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y))
  
  (k:. f:(kA). i,j:k. i<j  R(f(i);f(j)))

1

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))

13 steps

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