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. e
j
14. loc(j) = i
15.
(x after j) = (x when j)
(j [e, j])
