IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel star closure1 1. T : Type
2. R : TTProp
3. R2 : TTProp
4. Trans(T)(R2(_1,_2))
5. x,y:T. (xRy) (xR2y)
6. x : T 7. y : T 8. xR^0 y (xR2y) x = y
By:
ReduceExp -1 THEN SimpConcl
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html