Nuprl - Proof: extend intseg upperpart down 1 1 2

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

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:

Analyze7

Generated subgoals:

None

About:

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