Nuprl - Proof: split int seg all dom sfa

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

i,j:

i<j

(

F:({i..j

}

Prop). (

k:{i..j

}. F(k))

F(i) & (

k:{(i+1)..j

}. F(k)))

By:

UnivCD

Generated subgoal:

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))
6 steps

About:

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