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