is mentioned by

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]] 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 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]] 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]
Def affects_trace_rel(e;k;r) == reduce(x,y. affects_trace(e;k;x) y;false;r.args)	[affects_trace_rel]
Def rel_mentions_trace(r) == reduce(x,y. mentions_trace(x) y;false;r.args)	[rel_mentions_trace]
Def rel_primed_vars(r) == reduce(t,vs. term_primed_vars(t) @ vs;nil;r.args)	[rel_primed_vars]
Def subst_mentions_trace(as) == reduce(a,b. mentions_trace(2of(a)) b;false;as)	[subst_mentions_trace]

In prior sections: mb list 2 list 1 mb list 1 mb label mb automata 2

Try larger context: GenAutomata