is mentioned by

Thm* x:Label, u:Term. (x term_primed_vars(u)) (x term_vars(u))	[term_primed_vars_term_vars]
Thm* r:rel(), x:Label. rel_mentions(r;x) (x rel_vars(r))	[rel_mentions_iff]
Thm* x:Label, r:rel(). (x rel_vars(r)) (i:. i < ||r.args|| & (x term_vars(r.args[i])))	[member_rel_vars]
Thm* x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)	[term_subst2_addprime]
Def rel_mentions(r;x) == i:. i < ||r.args|| & (x term_vars(r.args[i]))	[rel_mentions]
Def covers_var(A;x) == fr:frame(). fr < fr A.frame | fr.var = x > & (a:Label. (a fr.acts) (ef:eff(). ef < ef A.eff | ef.kind = a & ef.smt.lbl = x > ))	[covers_var]

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

Try larger context: GenAutomata