IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel star symmetric11 1. T : Type
2. R : TTProp
3. a,b:T. (aRb) (bRa)
4. a : T 5. b : T 6. a (R^*) b R^-1 => R
By:
Unfolds [`rel_inverse`;`rel_implies`] 0 THEN Reduce 0 THEN EasyHyp
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)
R^-1 => R
