Nuprl - Proof: extend intseg upperpart down 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: extend intseg upperpart down 1 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

i
9. i = n-1

P(i)

By:	Rewrite by i = n-1 {a..b}

Generated subgoals:

None

About:

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