Thm* ds,da:Collection(dec()), st:Collection(SimpleType), de:sig(), rho:Decl
, e1:{1of([[de]] rho)}, s1,s2:{[[ds]] rho}, a:[[st]] rho, tr:trace_env([[da]] rho), u:Term
, t:SimpleType.
trace_consistent(rho;da;tr.proj;u) 
( x:Label. (x term_vars(u))  s1.x = s2.x) 
t term_types(ds;st;de;u)  [[u]] e1 s1 a tr = [[u]] e1 s2 a tr [[t]] rho | [term_mng_equal] |
Thm* 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) | [rel_subst_tc] |
Thm* r:rel(), as:(Label Term) List, ds:Collection(dec())
, da:Collection(SimpleType), de:sig().
tc(r;ds;da;de) 
( x:Label.
(x rel_primed_vars(r)) 
( t:SimpleType. mk_dec(x, t) ds  t term_types(ds;da;de;apply_alist(as;x;x))))

tc(rel_subst2(as;r);ds;da;de) | [rel_subst2_tc] |
Thm* r:rel(), x:Label. (x rel_primed_vars(r))  (x rel_vars(r)) | [rel_primed_vars_rel_vars] |
Thm* x:Label, r:rel().
(x rel_primed_vars(r))  ( i: . i < ||r.args|| & (x term_primed_vars(r.args[i]))) | [member_rel_primed_vars] |
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_primed_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_subst2(as;t)) | [term_subst2_tc] |
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] |