IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
symmetrized preorder32 1. T : Type
2. R : TTProp
3. Refl(T;x,y.R(x,y))
4. a,b,c:T. R(a,b) R(b,c) R(a,c)
5. a : T 6. b : T 7. c : T 8. R(a,b)
9. R(b,a)
10. R(b,c)
11. R(c,b)
R(c,a)
By:
FwdThru 4 [9;11]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T
a,b,c:T. R(a,b) 
R(b,c) 
R(c,a)
