Nuprl - Proof: split int seg all dom sfa 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: split int seg all dom sfa 1

1. i :

2. j :

3. i<j
4. F : {i..j

}

Prop

(

k:{i..j

}. F(k))

F(i) & (

k:{(i+1)..j

}. F(k))

By:	2 Times Analyze

Generated subgoals:

1 5. k:{i..j}. F(k)
F(i) & (k:{(i+1)..j}. F(k))
1 step

2 5. F(i) & (k:{(i+1)..j}. F(k))
k:{i..j}. F(k)
4 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	5. k:{i..j}. F(k) F(i) & (k:{(i+1)..j}. F(k))	1 step
2	5. F(i) & (k:{(i+1)..j}. F(k)) k:{i..j}. F(k)	4 steps