Nuprl - Proof: int segs from base by upper ind 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. P :

Prop
2. a :

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

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

c:{a..b

}. P(a,c))

P(a,b)

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

By:	k:, b:{a...}. b-ak P(a,b) Asserted

Generated subgoals:

1   k:, b:{a...}. b-ak  P(a,b)
5 steps

2 5. k:, b:{a...}. b-ak  P(a,b)
  b:{a...}. P(a,b)
1 step

About:

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

1	k:, b:{a...}. b-ak P(a,b)	5 steps
2	5. k:, b:{a...}. b-ak P(a,b) b:{a...}. P(a,b)	1 step