IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
intseg split1112 1. a :
2. b :
3. c : {a...b}
4. {a..b} ~ ({x:{a..b}| x<c }+{x:{a..b}| x<c })
{c..b} =ext {x:{a..b}| x<c }
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html