At: closed rel args 1 1 2 1 1
1. r: rel()
2. l: Term List
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
6. i:
7. term_free_vars(u) = nil
8. reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil
9. i < ||v||+1
10. i = 0
term_free_vars([u / v][0]) = nil
By: RWW "select_cons_hd" 0
Generated subgoals:None
About:
