1. es : ES
2. i : Id
3. P : {e:E| loc(e) = i }Prop
4. e@i.first(e)  P(e)
5. e@i.first(e)  P(pred(e))  P(e)
  e@i.P(e)

1

4. e:E. loc(e) = i  Id  first(e)  P(e) 5. e:E. loc(e) = i  Id  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  Id  P(k) 9. loc(j) = i  Id   P(j)

3 steps

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