Nuprl - Proof: int seg upper ind 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: int seg upper ind 1

1. P :

Prop
2. a :

b:{a...}. (

c:{a..b

}. P(a,c))

P(a,b)

b:{a...}. P(a,b)

By:	Enough that k:, b:{a...}. b-ak P(a,b) kBy (Auto THEN BackThru: Hyp:4 Using:[b-a])

Generated subgoal:

1 k:, b:{a...}. b-ak P(a,b)
5 steps

About:

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