is mentioned by

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]] rhom;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,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]
Def rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr) == list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[r.name]] rho 2of(e) ;r.args)	[rel_mng_2]

In prior sections: mb automata 2

Try larger context: GenAutomata