i:
. i < ||v|| & (x 
term_vars(v[i]))) 
(x reduce(
t,vs. term_vars(t) @ vs;nil;v))7. (
i:. i < ||v|| & (x term_vars(v[i]))) 
(x reduce(t,vs. term_vars(t) @ vs;nil;v))8. i:
9. i < ||v||+1
10. (x
term_vars([u / v][i]))
(x term_vars(u)) 
(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))7. (
i:. i < ||v|| & (x term_vars(v[i]))) (x reduce(t,vs. term_vars(t) @ vs;nil;v))8. (x
term_vars(u)) (x reduce(t,vs. term_vars(t) @ vs;nil;v)) i:. i < ||v||+1 & (x term_vars([u / v][i]))
