termlist_eq(v;v1)
i:
. i < ||v|| & v[i] = v1[i] i:. i < ||v||+1 & [u / v][i] = [u1 / v1][i]
b:Term List. termlist_eq(v;b) 
||v|| = ||b|| 
(i:. i < ||v|| & v[i] = b[i])
termlist_eq([u / v];v1) ||[u / v]|| = ||v1|| (i:. i < ||[u / v]|| & [u / v][i] = v1[i])
(term_eq(u;u1) & termlist_eq(v;v1))
i:. i < ||v||+1 & [u / v][i] = [u1 / v1][i]
| 1 | termlist_eq(v;v1) |
| 2 | 12. i:. i < ||v|| & v[i] = v1[i] i:. i < ||v||+1 & [u / v][i] = [u1 / v1][i] |
About:
 |  |  |  |  |  |
 |  |  |  |  |