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