Nuprl - Proof: and via all intseg notnull 1 3 1

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

1. a :

2. b :

3. P : {a..b

}

Prop
4. a<b
5. c :

6. b = c+1
7.

i:{a..c

}. P(i)
8. P(c)
9. i : {a..b

}
10. i = c

P(i)

By:	Rewrite by i = c {a..b}

Generated subgoals:

None

About:

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