IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
split int seg all dom sfa11 1. i : 2. j : 3. i<j 4. F : {i..j}Prop
5. k:{i..j}. F(k)
F(i) & (k:{(i+1)..j}. F(k))
By:
Auto THEN BackThru: Hyp:5
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
}
Prop
k:{i..j
F(i) & (
