a,b:Term List. termlist_eq(a;b) ||a|| = ||b|| (i:. i < ||a|| & a[i] = b[i])

1	1. a: Term List 2. b: Term List termlist_eq(nil;nil) 0 = 0 (i:. i < 0 & nil[i] = nil[i] Term)
2	1. a: Term List 2. u: Term 3. v: Term List 4. b:Term List. termlist_eq(v;b) ||v|| = ||b|| (i:. i < ||v|| & v[i] = b[i]) 5. b: Term List 6. u1: Term 7. v1: Term List 8. termlist_eq([u / v];v1) ||[u / v]|| = ||v1|| (i:. i < ||[u / v]|| & [u / v][i] = v1[i]) termlist_eq([u / v];[u1 / v1]) ||v||+1 = ||v1||+1 (i:. i < ||v||+1 & [u / v][i] = [u1 / v1][i])

About: