Nuprl - Proof: all int segs by upper ind 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: all int segs by upper ind 1 1 2

1. P :

Prop
2.

, b:{...a}. P(a,b)
3.

, b:{a+1...}. (

c:{a..b

}. P(a,c))

P(a,b)
4. a :

5. b : {a+1...}
6.

c:{a..b

}. P(a,c)

P(a,b)

By:	BackThru: Hyp:3

Generated subgoals:

None

About:

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