i:. reduce(t,vs. term_free_vars(t) @ vs;nil;l) = nil i < ||l|| term_free_vars(l[i]) = nil

1	i:. nil = nil Label List i < 0 term_free_vars(nil[i]) = nil
2	3. u: Term 4. v: Term List 5. i:. reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil i < ||v|| term_free_vars(v[i]) = nil i:. (term_free_vars(u) @ reduce(t,vs. term_free_vars(t) @ vs;nil;v)) = nil i < ||v||+1 term_free_vars([u / v][i]) = nil

About: