Nuprl - Proof: or via exist intseg notnull 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: or via exist intseg notnull 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)

By:

Auto

Generated subgoals:

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

2 7. (i:{a..c}. P(i))  P(c)
  i:{a..b}. P(i)
3 steps

About:

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

1	7. i:{a..b}. P(i) (i:{a..c}. P(i)) P(c)	4 steps
2	7. (i:{a..c}. P(i)) P(c) i:{a..b}. P(i)	3 steps