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