1. the_es : ES
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E
4. k:E. (k <loc j)  (e:E. (e  before(k))  (e <loc k))
5. e : E
6. first(j)
  (e  nil)  (e <loc j)

By:	Inst Thm* the_es:ES, j,e:E. first(j)  (e <loc j) [the_es;j;e] THEN ObviousContradiction [-1]

None

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