x:Label.
(
r:rel().
(r@0:rel(). r@0 
Q & r = mk_rel(r@0.name, map(
t.(t)';r@0.args)))
& (i:
. i < ||r.args|| & (x term_vars(r.args[i]))))
covers_var(A;x) Q term_vars(r.args[i]))
(x term_vars((r.args[i])'))t:Term. term_primed_vars((t)') ~ term_vars(t)
[r.args[i]]
x:Label, u:Term.
(x term_primed_vars(u)) (x term_vars(u))None
About:
| | | | | | |