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
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
11. (
11. (
(
ev[e, k].(x after ev) = (x when ev)) (x after k) = (x when e))
12. e : E
13.
first(j)
14. e = pred(j)
(e <loc pred(j))
15. loc(j) = i
16.
(ev[e, j].(x after ev) = (x when ev))
17. (x after j) = (x when j)
18. loc(e) = i
19.
first(j)
20. (x when j) = (x after pred(j))
e pred(j) 
