At: rel mentions trace iff 1 2 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) 
(i:. i < ||v|| & mentions_trace(v[i]))
7. i:
8. i < ||v||+1
9. mentions_trace([u / v][i])
10. i = 0
mentions_trace(u)
By:
HypSubstSq -1 -2
THEN
Reduce -2
Generated subgoals:None
About:
