Nuprl - Proof: int segs from base by upper ind 1 1 1

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

1. P :

Prop
2. a :

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

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

c:{a..b

}. P(a,c))

P(a,b)

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

P(a,b)

By:	CompNatInd Concl

Generated subgoal:

1 5. k :
6. k1:. k1<k (b:{a...}. b-ak1 P(a,b))
7. b : {a...}
8. b-ak
P(a,b)
4 steps

About:

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