At:
equal appends21
1.
T: Type
2.
a: T List
3.
u: T
4.
v: T List
5.
c,b,d:T List.
(v @ b) = (c @ d) (e:T List. v = (c @ e) & d = (e @ b) c = (v @ e) & b = (e @ d))
6.
c: T List b,d:T List. [u / (v @ b)] = d (e:T List. [u / v] = e & d = (e @ b) nil = [u / (v @ e)] & b = (e @ d))
By:
Obvious
Generated subgoals:
c,b,d:T List.
(v @ b) = (c @ d) 
(
e:T List. v = (c @ e) & d = (e @ b) 
c = (v @ e) & b = (e @ d))
