x,z,y,w:T List. ||x|| = ||z|| 
||y|| = ||w|| 
(x @ y) = (z @ w) x = z & y = wa,c,b,d:T List. (a @ b) = (c @ d) (
e:T List. a = (c @ e) & d = (e @ b) c = (a @ e) & b = (e @ d))as,bs:T List. ||as @ bs|| = ||as||+||bs|| l:T List. (l @ nil) ~ l