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
Dec(Q) ((P & Q) P Q))
-1
| 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:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |