is mentioned by

Thm* x:Label, r:rel(). (x rel_vars(r)) (i:. i < ||r.args|| & (x term_vars(r.args[i])))	[member_rel_vars]
Thm* r:rel(), de:sig(), i:. tc1(r;de) i < ||r.args|| rel_arg_typ(r.name;i;de) SimpleType	[rel_arg_typ_wf]
Thm* a,b:Term List. a = b ||a|| = ||b|| (i:. i < ||a|| & a[i] = b[i])	[unequal_termlists]
Def rel_mentions(r;x) == i:. i < ||r.args|| & (x term_vars(r.args[i]))	[rel_mentions]

In prior sections: int 1 bool 1 sqequal 1 int 2 list 1 mb nat num thy 1 mb list 1 mb collection mb list 2 prog 1 mb automata 1

Try larger context: GenAutomata