At: rel mentions trace iff 1 1 1
1. r: rel()
2. L: Term List
3. u: Term
4. v: Term List
5. reduce(
x,y. mentions_trace(x) 
y;false;v) 
(
i:
. i < ||v|| & mentions_trace(v[i]))
6. reduce(x,y. mentions_trace(x) y;false;v)
7. i:
8. i < ||v||
9. mentions_trace(v[i])
mentions_trace([u / v][(i+1)])
By:
RWW "select_cons_tl" 0
THEN
ArithSimp 0
Generated subgoals:None
About:
