true v(
eq) v1
}
T
T
x:T. eq(x,x)
x,y:T. eq(x,y) 
eq(y,x)
x,y,z:T. eq(x,y) 
eq(y,z) eq(x,z)
eq) remove(eq;u;v1) v(eq) v1
eq) (u1.remove(eq;u;v1))
v(eq) (u1.v1)
| 1 | 15. eq(v,u1) = true true |
| 2 | 15. eq(v,u1) = false v(eq) v1 |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |
 |