x 
{x:T| if eq(x,u)
true
else x(eq) v fi }}
(eq)M 
(
x:{x:T| x(eq) v }. x(eq) M)
xv.x(eq) M
(eq)M
eq) v }
eq) M
x:{x:T| if eq(x,u) true else x(eq) v fi }. x(eq) M
| 1 | x {x:T| if eq(x,u) true else x(eq) v fi } |
About:
 |  |  |  |
 |  |  |  |  |
 |