Nuprl - Proof: split int seg exist dom sfa 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: split int seg exist 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:

Auto

Generated subgoals:

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

2 5. F(i)  (k:{(i+1)..j}. F(k))
  k:{i..j}. F(k)
3 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))	4 steps
2	5. F(i) (k:{(i+1)..j}. F(k)) k:{i..j}. F(k)	3 steps