Nuprl - Proof: and via all intseg notnull

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: and via all intseg notnull

a,b:

, P:({a..b

}

Prop).

a<b

(

. b = c+1

((

i:{a..b

}. P(i))

(

i:{a..c

}. P(i)) & P(c)))

By:

UnivCD

Generated subgoal:

1 1. a :
2. b :
3. P : {a..b}Prop
4. a<b
5. c :
6. b = c+1
(i:{a..b}. P(i)) (i:{a..c}. P(i)) & P(c)
6 steps

About:

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