1. T : Type
2. R : TTProp
3. Trans x,y:T. R(x,y)
4. a : T
5. a' : T
6. b : T
7. b' : T
8. R(a,b)
9. R(b,a)
10. R(a',b')
11. R(b',a')
12. R(b,b')
  R(a,a')

By:	FwdThru Thm* R:(TTProp).  Thm* (Trans x,y:T. R(x,y)) Thm*  Thm* (a,a',b,b':T. R(b,a)  R(a',b')  R(a,a')  R(b,b')) [3]

1

13. a,a',b,b':T. R(b,a)  R(a',b')  R(a,a')  R(b,b')   R(a,a')

1 step

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