r:rel(), as:(Label
Term) List. 1of(unzip(as)) = rel_vars(r) 
rel_subst2(as;(r)') = rel_subst(as;r)r:rel(), x:Label. rel_mentions(r;x) 
(x 
rel_vars(r))x:Label, r:rel(). (x rel_vars(r)) (
i:
. i < ||r.args|| & (x term_vars(r.args[i])))
t,vs. term_vars(t) @ vs;nil;r.args)
is mentioned by
| Thm* r:rel(), as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) rel_subst2(as;(r)') = rel_subst(as;r) | [rel_subst2_addprime] |
| 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] |
Try larger context:
GenAutomata