At:
assert termlist eq2
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]
term_eq(u;u1)termlist_eq(v;v1)
By:
RW assert_pushdownC 0
THEN
Analyze 0
Generated subgoals:
term_eq(u;u1)
b:Term List. termlist_eq(v;b) 
v = b
termlist_eq(v;v1)
