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