true & u(
eq) M u(eq) v & u(eq) M}
T
T
x,y:T. eq(x,y) 
x = y
M:T List. 
disjoint(eq;v;M) 
(
x:T. x(eq) v & x(eq) M)
u(eq) M
if eq(u,u)
true else u(eq) v fi & u(eq) M
| 1 | 11. eq(u,u) = true true & u(eq) M |
| 2 | 11. eq(u,u) = false u(eq) v & u(eq) M |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |