r:rel(), x:Label. rel_mentions(r;x) 
(x 
rel_vars(r))x:Label. rel_mentions(r;x) 
covers_var(A;x)
r:rel(). r p & rel_mentions(r;x)i:
. i < ||r.args|| & (x term_vars(r.args[i]))
is mentioned by
| Thm* r:rel(), x:Label. rel_mentions(r;x) (x rel_vars(r)) | [rel_mentions_iff] |
| Def covers_rel(A;r) == x:Label. rel_mentions(r;x) covers_var(A;x) | [covers_rel] |
| Def pred_mentions(p;x) == r:rel(). r p & rel_mentions(r;x) | [pred_mentions] |
Try larger context:
GenAutomata