es:ES, i,x:Id, T:Type, I:(T
Prop).
Thm* (vartype(i;x)
r T) & e@i.first(e) 
I((x when e))
Thm*
Thm*
e@i.I((x when e)) I((x after e)) @i always.I(x)es:ES, i:Id, P:({e:E| loc(e) = i 
Id }Prop).
Thm*
e@i.P(e) 
e@i.first(e) P(e) & e@i.
first(e) P(pred(e)) P(e)