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]
Thm* ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl , t:Term, s:{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[st1]] rho , tr:trace_env([[da]] rho). trace_consistent(rho;da;tr.proj;t) a term_types(ds;st1;de;t) [[t]] e s v tr [[a]] rho	[term_typing]
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]
Thm* ds,da:Collection(dec()), st:Collection(SimpleType), de:sig(), rho:Decl , e1:{1of([[de]] rho)}, s1,s2:{[[ds]] rho}, a:[[st]] rho, tr:trace_env([[da]] rho), u:Term , t:SimpleType. trace_consistent(rho;da;tr.proj;u) (x:Label. (x term_vars(u)) s1.x = s2.x) t term_types(ds;st;de;u) [[u]] e1 s1 a tr = [[u]] e1 s2 a tr [[t]] rho	[term_mng_equal]
Thm* da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label. trace_consistent(rho;da;tr.proj;trace(y1)) tr.y1 [[lbl_pr( < Trace, y1 > )]] rho	[tproj_w_f2]
Thm* ds:Collection(dec()), rho:Decl, a:([[ds]] rho), x:Label. mk_dec(kind(a), x) ds value(a) rho(x)	[sigma_decls_mng_value2]
Thm* d1,d2:Collection(dec()), rho:Decl, u:([[d1]] rho). d1 = d2 u ([[d2]] rho)	[sigma_decls_mng_functionality]
Thm* ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label , t:SimpleType. t dec_lookup(ds;x) s.x [[t]] rho	[record_select_wf_decls_mng2]
Thm* ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label , t:SimpleType. mk_dec(x, t) ds s.x [[t]] rho	[record_select_wf_decls_mng]
Thm* ds:Collection(dec()), rho:Decl, a:([[ds]] rho). value(a) [[dec_lookup(ds;kind(a))]] rho	[sigma_decls_mng_value]
Thm* da:Collection(dec()), rho:Decl, k:Label, w:[[dec_lookup(da;k)]] rho. < k,w > ([[da]] rho)	[sigma_decls_mng2]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds2 ds1 r {[[ds2]] rho}	[decls_mng_monotone]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds2 ds1 r {[[ds2]] rho}	[decls_mng_record_subtype]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:([[ds1]] rho). ds1 = ds2 r ([[ds2]] rho)	[decls_mng_functionality_sigma]
Thm* ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds1 = ds2 r {[[ds2]] rho}	[decls_mng_functionality]
Thm* da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label. tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List	[tproj_w_f]
Thm* d1,d2:Collection(dec()), rho:Decl, u:([[d1]] rho). d2 d1 u ([[d2]] rho)	[sigma_decls_mng_monotone]
Thm* ds1,ds2:Collection(dec()), x,y:Label, rho:Decl , v:[[ds1]] rho(x). (d:dec(). d ds2 d.lbl = y mk_dec(x, d.typ) ds1) v [[ds2]] rho(y)	[decls_mng_rename_member]
Thm* d:dec(), rho:Decl, s:{[[d]] rho}. s {[[ < d > ]] rho}	[decls_mng_singleton]
Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x) , a:SimpleType. mk_dec(x, a) ds y [[a]] rho	[decls_mng_subtype]
Thm* ds1,ds2:Collection(dec()), x:Label, rho:Decl, v:[[ds1]] rho(x). (d:dec(). d ds2 d.lbl = x d ds1) v [[ds2]] rho(x)	[decls_mng_member]
Thm* v:Top, rho:Decl, x:Label. v [[ < > ]] rho(x)	[empty_decls_mng]
Def trace_consistent(rho;da;R;t) == g:Label. term_mentions_guard(g;t) subtype_rel(({a:([[da]] rho)| (R(g,kind(a))) } List); (rho(lbl_pr( < Trace, g > ))))	[trace_consistent]

Try larger context: GenAutomata