At: member rel primed vars 3 1 1 1
1. x: Label
2. name: relname()
3. r1: Term List
4. u: Term
5. v: Term List
6. (
i:
. i < ||v|| & (x 
term_primed_vars(v[i]))) 
(x reduce(
t,vs. term_primed_vars(t) @ vs;nil;v))
7. i:
8. i < ||v||+1
9. 
i = 0
10. (x term_primed_vars([u / v][i]))
(x term_primed_vars(v[(i-1)]))
By:
Subst' ([u / v][i] = v[(i-1)]) -1
THEN
RWW "select_cons_tl" 0
Generated subgoals:None
About:
