a,b,a',b':. (a ~ a')  (b ~ b')  ((a ~ b)  (a' ~ b'))

By:	BackThru Thm* R:(TTProp).  Thm* (EquivRel x,y:T. R(x,y)) Thm*  Thm* (a,a',b,b':T. R(a,b)  R(a',b')  (R(a,a')  R(b,b')))

1

EquivRel x,y:. x ~ y

1 step

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