At:
assert termlist eq221
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.
[u / v] = [u1 / v1]
v = v1
By:
ApFunToHypEquands `z' tl(z) (Term List) -1
THEN
Reduce -1
Generated subgoals:
b:Term List. termlist_eq(v;b) 
v = b
v = v1