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

By:	Repeat (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) THEN Try BackThruSomeHyp

1

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

7 steps

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