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

1

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

5 steps

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