IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
split int seg exist dom sfa121 1. i : 2. j : 3. i<j 4. F : {i..j}Prop
5. F(i)
k:{i..j}. F(k)
By:
Witness: i
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
}
Prop
k:{i..j
