x:{x:T| if eq(x,u)
true
else x(
eq) v fi }. P(x)
P(u)x:{x:T| if eq(x,u) true else x(eq) v fi }. P(x) xv.P(x)}
Type
x:{x:T| x(eq) v }. P(x)) 
xv.P(x)
(x:{x:T| if eq(x,u) true else x(eq) v fi }. P(x)) P(u) & xv.P(x)
| 1 | 8. x:{x:T| if eq(x,u) true else x(eq) v fi }. P(x) P(u) |
| 2 | 8. x:{x:T| if eq(x,u) true else x(eq) v fi }. P(x) xv.P(x) |
About:
 |  |  |  |  |
 |  |  |  |  |  |