At:
rel mentions iff
1
2
2
2
1
1.
r: rel()
2.
x: Label
3.
l: Term List
4.
u: Term
5.
v: Term List
6.
(x 
reduce(
t,vs. term_vars(t) @ vs;nil;v))
7.
i: 
8.
i < ||v||
9.
(x term_vars(v[i]))
10.
(x reduce(t,vs. term_vars(t) @ vs;nil;v))
(x term_vars([u / v][(i+1)]))
By:
RWW "select_cons_tl" 0
THEN
ArithSimp 0
Generated subgoals:
None
About:
