At:
assert termlist eq21
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)
By:
BackThru
Thm*a,b:Term. term_eq(a;b) a = b
Generated subgoal:
u = u1
b:Term List. termlist_eq(v;b) 
v = b
