Nuprl - Proof: int seg upper ind 1 1 1 1

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

1. P :

Prop
2. a :

b:{a...}. (

c:{a..b

}. P(a,c))

P(a,b)
4. k :

k1:

. k1<k

(

b:{a...}. b-a

P(a,b))
6. b : {a...}
7. b-a

k
8. k = 0

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