Nuprl - Proof: extend intseg upperpart down

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

a,b:

, P:({a..b

}

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

P(n-1)

(

i:{a..b

}. n

P(i))

(

i:{a..b

}. n-1

P(i))

By:	RemoveGuards Concl THEN 6 Times Analyze

Generated subgoal:

1 1. a :
2. b :
3. P : {a..b}Prop
4. n : {(a+1)..(b+1)}
5. P(n-1)
6. i:{a..b}. ni P(i)
i:{a..b}. n-1i P(i)
4 steps

About:

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