Nuprl - Proof: extend intseg upperpart down 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: extend intseg upperpart down 1 1

1. a :

2. b :

3. P : {a..b

}

Prop
4. n : {(a+1)..(b+1)

}
5. P(n-1)
6. i : {a..b

}
7. n

P(i)
8. n-1

P(i)

By:	Decide: i = n-1

Generated subgoals:

1 9. i = n-1
P(i)
1 step

2 9. i = n-1
P(i)
1 step

About:

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