Nuprl - Proof: or via exist intseg notnull 1 2

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

1. a :

2. b :

3. P : {a..b

}

Prop
4. a<b
5. c :

6. b = c+1
7. (

i:{a..c

}. P(i))

P(c)

i:{a..b

}. P(i)

By:

Analyze-1

Generated subgoals:

1 7. i:{a..c}. P(i)
i:{a..b}. P(i)
1 step

2 7. P(c)
i:{a..b}. P(i)
1 step

About:

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

1	7. i:{a..c}. P(i) i:{a..b}. P(i)	1 step
2	7. P(c) i:{a..b}. P(i)	1 step