At:
append one one2
1.
T: Type
2.
x: T List
3.
z: T List
4.
y: T List
5.
w: T List
6.
||x|| = ||z|| ||y|| = ||w||
7.
(x @ y) = (z @ w)
8.
e: T List
9.
x = (z @ nil) & w = (nil @ y) z = (x @ nil) & y = (nil @ w)
x = z & y = w
By:
Reduce -1
THEN
RWO
Thm*l:T List. (l @ nil) ~ l
-1
THEN
Analyze -1
Generated subgoals:
||y|| = ||w|| 
x = z & y = w
l:T List. (l @ nil) ~ l
-1