T:Type, R:(TTProp), x,y,z:T. (x (R^*) y)  (y (R^*) z)  (x (R^*) z)

1

1. T : Type 2. R : TTProp 3. x : T 4. y : T 5. z : T 6. n1 :  7. x R^n1 y 8. n :  9. y R^n z   x R^n1+n z

1 step

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