| Rank | Theorem | Name |
| 3 |
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] |
| cites |
| 0 |
Thm* L:T List. 0 < ||L|| (L ~ [hd(L) / tl(L)]) | [list_decomp] |
| 2 |
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] |
| 0 |
Thm* l:A List. ||l|| 1 ||tl(l)|| = ||l||-1 | [length_tl] |