1. es : ES
2. x : Id
3. i : Id
4. T : Type
5. x,y:T. Dec(x = y)
6. vartype(i;x) r T
7. e:E. loc(e) = i  (x when e)  T
8. e:E. loc(e) = i  (x after e)  T
  e',e:E.
  e  e' 
  
  loc(e') = i  Id
  
  (ev[e, e'].(x after ev) = (x when ev)  T)
  
  (x after e') = (x when e)  T

By:	LocLessInd THENA (Auto THEN BackThruSomeHyp THEN Try (Analyze -1 THEN Complete Auto)) THEN AllHyps (h. (Unfold `es-le` h THEN Analyze h (THENL ([Unfold `es-locl` h THEN Complete Auto;HypSubst h 0])

1

9. WellFnd{i}(E;x,y.(x <loc y)) 10. j : E 11. k:E.  11. (k <loc j) 11.  11. (e:E.  11. (e  k  11. ( 11. (loc(k) = i  Id 11. ( 11. ((ev[e, k].(x after ev) = (x when ev)  T) 11. ( 11. ((x after k) = (x when e)  T)   e:E.    e  j       loc(j) = i  Id      (ev[e, j].(x after ev) = (x when ev)  T)  (x after j) = (x when e)  T

43 steps

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