Thm* ds,da:Collection(dec()), de:sig(), rho:Decl, st1:Collection(SimpleType)
, e1:{1of([[de]] rho)}, s:{[[ds]] rho}, a:[[st1]] rho, tr:trace_env([[da]] rho), l:Term List.
( i: ||l||. trace_consistent(rho;da;tr.proj;l[i])) 
( ls:SimpleType List, f:reduce( s,m. [[s]] rho m;Prop;ls).
||ls|| = ||l|| & ( i: . i < ||l||  ls[i] term_types(ds;st1;de;l[i])) 
list_accum(x,t.x([[t]] e1 s a tr);f;l) Prop) | [rel_mng_lemma] |
Thm* ds,da:Collection(dec()), de:sig(), rho:Decl, st1:Collection(SimpleType)
, e1:{1of([[de]] rho)}, s,s':{[[ds]] rho}, a:[[st1]] rho, tr:trace_env([[da]] rho), l:Term List.
( i: ||l||. trace_consistent(rho;da;tr.proj;l[i])) 
( ls:SimpleType List, f:reduce( s,m. [[s]] rho m;Prop;ls).
||ls|| = ||l|| & ( i: . i < ||l||  ls[i] term_types(ds;st1;de;l[i])) 
list_accum(x,t.x([[t]] e1 s s' a tr);f;l) Prop) | [rel_mng_2_lemma] |
Thm* ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl
, t:Term, s:{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[st1]] rho
, tr:trace_env([[da]] rho).
trace_consistent(rho;da;tr.proj;t)  a term_types(ds;st1;de;t)  [[t]] e s v tr [[a]] rho | [term_typing] |
Thm* ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl
, t:Term, s,s':{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[da]] rho
, tr:trace_env([[daa]] rho).
trace_consistent(rho;daa;tr.proj;t)  a term_types(ds;da;de;t)  [[t]] e s s' v tr [[a]] rho | [term_typing2] |
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* ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType)
, de:sig(), t:Term.
ds1 ds2 
da1 da2  ( a:SimpleType. a term_types(ds1;da1;de;t)  a term_types(ds2;da2;de;t)) | [term_types_monotone_member] |
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] |
Thm* t:Term, ds:Collection(dec()), da1,da2:Collection(SimpleType)
, de:sig(). closed_term(t)  term_types(ds;da1;de;t) = term_types(ds;da2;de;t) | [term_types_closed] |
Thm* ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig()
, t:Term. ds1 ds2  da1 da2  term_types(ds1;da1;de;t) term_types(ds2;da2;de;t) | [term_types_monotone] |
Thm* ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType)
, de:sig(), t:Term. ds1 = ds2  da1 = da2  term_types(ds1;da1;de;t) = term_types(ds2;da2;de;t) | [term_types_functionality] |
Thm* t:Term, ds,da,de:Top.
term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t) | [term_types_unprime] |
Thm* t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t) | [term_types_addprime] |
Def tc_smt(s;ds;da;de)
== mk_dec(s.lbl, s.typ) ds & s.typ term_types(ds;da;de;s.term) | [tc_smt] |
Def tc(r;ds;da;de)
== Case(r.name)
Case eq(Q) = >
||r.args|| = 2 & Q term_types(ds;da;de;r.args[0]) & Q term_types(ds;da;de;r.args[1])
Case R = >
||de.rel(R)|| = ||r.args||
& ( i: . i < ||r.args||  (de.rel(R))[i] term_types(ds;da;de;r.args[i]))
Default = > False | [tc] |