IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel inverse exp2 1. T : Type
2. R : TTProp
3. n : 4. 0<n 5. x,y:T. (xR^n-1^-1 y) (xR^-1^n-1 y)
x,y:T. (xR^n^-1 y) (xR^-1^ny)
By:
Unfold `rel_inverse` 0 THEN Reduce 0 THEN Fold `rel_inverse` 0