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
8. e : E
9.
e:E. loc(e) = i 
(x when e) 
T
10.
e:E. loc(e) = i (x after e) T
11. e
e'
12. loc(e') = i
13.
(x after e') = (x when e)
14. ev : {e:E| loc(e) = i }
15. (ev
[e, e'])
16.
(x after ev) = (x when ev)
17. e1 : E
18. e
e1
19. loc(e1) = loc(e')
20. (e1 < e')
vartype(loc(e1);x) r T
