| 4 | | | Thm*  r:rel(), ds,da:Collection(dec()), de:sig(), rho:Decl, st1:Collection(SimpleType), e:{[[de]] rho}, s,s':{[[ds]] rho}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r)   tc(r;ds;st1;de) rel_mng_2(r; rho; ds; st1; de; e; s; s'; a; tr)  Prop | [rel_mng_2_wf] |
| 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] |