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