At:
equal appends case1221
1.
T: Type
2.
x1: T List
3.
u: T
4.
v: T List
5.
z,x2,x3:T List. ||v||||z|| (v @ x2) = (z @ x3) (z':T List. z = (v @ z') & x2 = (z' @ x3))
6.
z: T List
7.
u1: T
8.
v1: T List
9.
x2,x3:T List.
||v||+1||v1|| [u / (v @ x2)] = (v1 @ x3) (z':T List. v1 = [u / (v @ z')] & x2 = (z' @ x3))
10.
x2: T List
11.
x3: T List
12.
||v||+1||v1||+1
13.
[u / (v @ x2)] = [u1 / (v1 @ x3)]
(v @ x2) = (v1 @ x3)
By:
Obvious
Generated subgoals: