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

1

1. T : Type 2. R : TTProp 3. R' : TTProp 4. x,y:T. R(x,y)  R'(x,y)   (a,b,c:T. R(b,a)  R(c,b)  R(c,a))      (a,b,c:T. R'(b,a)  R'(c,b)  R'(c,a))

2 steps

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