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

By:	ParallelOp -1 THEN Try (BackThruSomeHyp (THEN (FwdThru Thm* es:ES, e,e':E. e  e'   loc(e) = loc(e')  Id [-1])

1

18. ev : E 19. e  ev  & ev  e'  & (x after ev) = (x when ev)  T   ev  e'  & (x after ev) = (x when ev)  T

Auto

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