Nuprl - Proof: or via exist intseg notnull 1 1 1

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

1. a :

2. b :

3. P : {a..b

}

Prop
4. a<b
5. c :

6. b = c+1
7. i : {a..b

}
8. P(i)

(

i:{a..c

}. P(i))

P(c)

By:	SimilarTo: i<c i = c

Generated subgoals:

1 9. i<c
i:{a..c}. P(i)
1 step

2 9. i = c
P(c)
1 step

About:

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