IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel star symmetric12 1. T : Type
2. R : TTProp
3. a,b:T. (aRb) (bRa)
4. a : T 5. b : T 6. a (R^*) b b (R^-1^*) a
By:
RWO "rel_inverse_star<" 0 THEN Unfold `rel_inverse` 0 THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T
a,b:T. (a R b) 
(b R a)
b (R^-1^*) a
