LOCAL M2. Append(Nil, x, x). Append(Cons(u,x),y,Cons(u,z)) <- Append(x,y,z). Append3(x,y,z,u) <- Append(x,y,w) & Append(w,z,u).