es:ES, x,i:Id, T:Type.
Thm* (
x,y:T. Dec(x = y 
T))
Thm*
Thm* (vartype(i;x)
r T)
Thm*
Thm* (
e',e:E.
Thm* (e
e'
Thm* (
Thm* (loc(e') = i
Id
Thm* (
Thm* (
(x after e') = (x when e) T
Thm* (
Thm* ((
ev:E. e ev & ev e' & (x after ev) = (x when ev) T))F:(A
Prop), L:A List. (k:A. Dec(F(k))) Dec((kL.F(k)))the_es:ES, e,e':E.
Thm* (e <loc e')
first(e') & e = pred(e') E 
(e <loc pred(e'))L:A List, x:A. (A r B) (x L) (x L)the_es:ES. Trans x,y:E. x y the_es:ES, j:E. first(j) (pred(j) <loc j)the_es:ES, e:E. first(e) loc(pred(e)) = loc(e) Ides:ES, e,e':E. [e, e'] {ev:E| loc(ev) = loc(e') Id } Listes:ES, e,e':E. e e' loc(e) = loc(e') Ides:ES, e,e',ev:E. (ev [e, e']) e ev & ev e' (L:A List, x:B. (x L) (x L))