u.v = (nil @ (x.v)) & v = (nil @ v)
}
T
T
x,y:T. eq(x,y) 
x = y
eq) v 
(
M,N:T List. v = (M @ (x.N)) & remove(eq;x;v) = (M @ N))
True (M,N:T List. u.v = (M @ (x.N)) & v = (M @ N))
| 1 | u.v = (nil @ (x.v)) & v = (nil @ v) |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |
 |