Type5. L: T List
6. u: T
7. v: T List
8. (
x:{x:T| x(
eq) v }. P(x)) 
xv.P(x)9. eq(u,u) = false
10. eq(u,u)
u = u
u(eq) v}
TT
x,y:T. eq(x,y) x = y
Type
x:{x:T| x(eq) v }. P(x)) xv.P(x)
u(eq) v
| 1 | 4. P: TType 5. L: T List 6. u: T 7. v: T List 8. ( x:{x:T| x(eq) v }. P(x)) xv.P(x)9. eq(u,u) = false 10. eq(u,u) u = u u(eq) v |
About:
 |  |  |  |  |  |
 |  |  |  |  |
 |