1. T : Type
2. R : TTProp
3. a,b:T. (a R b)  (b R a)
4. a : T
5. b : T
6. a (R^*) b
  b (R^*) a

By:	Using [`R1',R^-1] (BackThru (Thm* R1,R2:(TTProp), x,y:T. R1 => R2  (x (R1^*) y)  (x (R2^*) y))

1	R^-1 => R	1 step
2	b (R^-1^*) a	1 step

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