T:Type, R:(TTProp).
  (Trans x,y:T. R(x,y))
  
  (a,a',b,b':T. R(b,a)  R(a',b')  R(a,a')  R(b,b'))

1

1. T : Type 2. R : TTProp 3. a,b,c:T. R(a,b)  R(b,c)  R(a,c) 4. a : T 5. a' : T 6. b : T 7. b' : T 8. R(b,a) 9. R(a',b') 10. R(a,a')   R(b,b')

1 step

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