At:
assert termlist eq1
1.
a: Term List
2.
u: Term
3.
v: Term List
4.
b:Term List. termlist_eq(v;b) v = b
5.
b: Term List
6.
u1: Term
7.
v1: Term List
8.
termlist_eq([u / v];v1) [u / v] = v1
9.
termlist_eq([u / v];v1) ([u / v] = v1)
10.
term_eq(u;u1)termlist_eq(v;v1)
[u / v] = [u1 / v1]
b:Term List. termlist_eq(v;b) 
v = b
termlist_eq(v;v1)
