(
u(
eq) M & disjoint(eq;v;M)) 
(
x:T. if eq(x,u)
true else x(eq) v fi & x(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)
M:T List. disjoint(eq;(u.v);M) (x:T. x(eq) (u.v) & x(eq) M)
| 1 | 9. M: T List (u(eq) M & disjoint(eq;v;M)) (x:T. if eq(x,u) true else x(eq) v fi & x(eq) M) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |