term_vars(u))
i:
. i < ||v||+1 & (x term_vars([u / v][i])) reduce(
t,vs. term_vars(t) @ vs;nil;v)) i:. i < ||v||+1 & (x term_vars([u / v][i]))i:. i < ||v|| & (x term_vars(v[i]))) 
(x reduce(t,vs. term_vars(t) @ vs;nil;v))
i:. i < ||v|| & (x term_vars(v[i]))) 
(x reduce(t,vs. term_vars(t) @ vs;nil;v))
term_vars(u)) 
(x reduce(t,vs. term_vars(t) @ vs;nil;v))
i:. i < ||v||+1 & (x term_vars([u / v][i]))
| 1 | 8. (x term_vars(u)) i:. i < ||v||+1 & (x term_vars([u / v][i])) |
| 2 | 8. (x reduce(t,vs. term_vars(t) @ vs;nil;v)) i:. i < ||v||+1 & (x term_vars([u / v][i])) |
About:
 |  |  |  |  |  |  |  |  |  |