Nuprl - Proof: alle-at-iff 3 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: alle-at-iff 3 1

1. es : ES
2. i : Id
3. P : {e:E| loc(e) = i }

Prop
4.

e:E. loc(e) = i

first(e)

P(e)
5.

e:E. loc(e) = i

first(e)

P(pred(e))

P(e)
6. WellFnd{i}(E;x,y.(x <loc y))
7. j : E
8.

k:E. (k <loc j)

loc(k) = i

P(k)
9. loc(j) = i

P(j)

By:	Decide first(j)

Generated subgoals:

1 10. first(j)
P(j)
1 step

2 10. first(j)
P(j)
1 step

About:

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