es:ES, x,i:Id, T:Type.
  (x,y:T. Dec(x = y  T))
  
  (vartype(i;x) r T)
  
  (e',e:E.
  (e  e' 
  (
  (loc(e') = i  Id
  (
  ((x after e') = (x when e)  T
  (
  ((ev:E. e  ev  & ev  e'  & (x after ev) = (x when ev)  T))

By:	RepeatFor 8 (Analyze 0 THENA Complete Auto) THEN AssertBY (e:E. loc(e) = i  (x when e)  T) (Auto THEN DoSubsume THEN HypSubst -1 0) THEN AssertBY (e:E. loc(e) = i  (x after e)  T) (Auto THEN DoSubsume THEN HypSubst -1 0)

1

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

63 steps

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