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]
Def rel_subst2(as;r) == mk_rel(r.name, map(t.term_subst2(as;t);r.args))	[rel_subst2]
Def (r)' == mk_rel(r.name, map(t.(t)';r.args))	[rel_addprime]
Def rel_free_vars(r) == reduce(t,vs. term_free_vars(t) @ vs;nil;r.args)	[rel_free_vars]
Def rel_unprime(r) == mk_rel(r.name, map(t.unprime(t);r.args))	[rel_unprime]
Def rel_subst(as;r) == mk_rel(r.name, map(t.term_subst(as;t);r.args))	[rel_subst]
Def rel_mentions(r;x) == i:. i < ||r.args|| & (x term_vars(r.args[i]))	[rel_mentions]
Def rel_vars(r) == reduce(t,vs. term_vars(t) @ vs;nil;r.args)	[rel_vars]

In prior sections: mb automata 1

Try larger context: GenAutomata