13. i < ||v||
14.
v[i] = v1[i]
i+1 < ||v||+1 & [u / v][(i+1)] = [u1 / v1][(i+1)]
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|| & v[i] = v1[i]
i:. i < ||v||+1 & [u / v][i] = [u1 / v1][i]
| 1 | 12. i: 13. i < ||v|| 14. v[i] = v1[i] i+1 < ||v||+1 & [u / v][(i+1)] = [u1 / v1][(i+1)] |
About:
 |  |  |  |  |  |
 |  |  |  |  |