x1,z,x2,x3:T List. ||x1|| = ||z|| 
(x1 @ x2) = (z @ x3) x1 = z & x2 = x3x1,z,x2,x3:T List. ||x1||
||z|| (x1 @ x2) = (z @ x3) (
z':T List. z = (x1 @ z') & x2 = (z' @ x3))l:T List. (l @ nil) ~ las,bs:T List. ||as @ bs|| = ||as||+||bs||