Nuprl - Proof: or via exist intseg notnull

(9steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc

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

a,b:

, P:({a..b

}

Prop).

a<b

(

c:

. 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)
8 steps

About:

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

(9steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc