At: rel mentions trace iff 1 2 2
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
reduce(x,y. mentions_trace(x) y;false;v)
By:
BackThruSomeHyp
THEN
InstConcl [i-1]
THEN
RWW "select_cons_tl" -2
Generated subgoals:None
About:
