IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
trans rel self functionality1 1. T : Type
2. R : TTProp
3. a,b,c:T. R(a,b) R(b,c) R(a,c)
4. a : T 5. a' : T 6. b : T 7. b' : T 8. R(b,a)
9. R(a',b')
10. R(a,a')
R(b,b')
By:
(FwdThru 3 [9;10]) THEN (FwdThru 3 [8;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(b,b')
