T:Type, x,z,y,w:T List. ||x|| = ||z|| ||y|| = ||w|| (x @ y) = (z @ w) x = z & y = w

1	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 @ e) & w = (e @ y) z = (x @ e) & y = (e @ w) e = nil	3 steps
2	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	1 step

About: