Thm* t:Term, s:SimpleType, as:(Label Term) List, ds:Collection(dec())
, da:Collection(SimpleType), de:sig().
s term_types(ds;da;de;t) 
( x:Label.
(x term_vars(t)) 
( t:SimpleType. mk_dec(x, t) ds  t term_types(ds;da;de;apply_alist(as;x;x))))

s term_types(ds;da;de;term_subst(as;t)) | [term_subst_tc] |
Thm* t:Term, as:(Label Term) List.
( x:Label. unprime(apply_alist(as;x;x)) = x)  unprime(term_subst(as;t)) = unprime(t) | [trivial_term_subst] |
Thm* as:(Label Term) List, g:Label, t:Term.
subst_mentions_trace(as)  term_mentions_guard(g;term_subst(as;t))  term_mentions_guard(g;t) | [term_subst_mentions_guard] |