r:rel(), as:(Label
Term) List, ds:Collection(dec())
, da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) 
(x:Label.
(x 
rel_vars(r))
(t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x))))
tc(rel_subst(as;r);ds;da;de)t:Term, s:SimpleType, as:(LabelTerm) 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))