2. x : Id
3. k : Knd
4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : State(ds)
ma-valtype(da; k)ds(x)?Void
7. es : ES
8. w : World
9. p : FairFifo
10. PossibleWorld(d-single-effect(i; ds; da; k; x; f);w)
11. es = ES(w)
12.
x:Id. vartype(i;x) 
r ds(x)?Top
13.
e:E. loc(e) = i 
(valtype(e) r ma-valtype(da; kind(e)))
14. e : E
15. loc(e) = i
16. kind(e) = k
(x after e) 
ds(x)?Top
