| 3 | | | Thm*  r:rel(), i: , ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, s,s':{[[ds]] rho}, e:{1of([[de]] rho)}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r)   tc(r;ds;st1;de) i < ||r.args|| [[r.args[i]]] e s s' a tr  [[rel_arg_typ(r.name;i;de)]] rho | [rel_arg_typing2] |
| 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] |