Nuprl - Proof: extend intseg upperpart down 1

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

1. a :

2. b :

3. P : {a..b

}

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

}
5. P(n-1)
6.

i:{a..b

}. n

P(i)

i:{a..b

}. n-1

P(i)

By:	SimilarTo Hyp:-1

Generated subgoal:

1 6. i : {a..b}
7. ni P(i)
8. n-1i
P(i)
3 steps

About:

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