(
M,N:T List. nil = (M @ (x.N))) 
False8. v: T List
9. (
M,N:T List. v = (M @ (x.N))) x(
eq) v (M,N:T List. u.v = (M @ (x.N))) if eq(x,u)
true
else x(eq) v fi}
T
T
x,y:T. eq(x,y) 
x = y
M,N:T List. L = (M @ (x.N))
x(eq) L
| 1 | (M,N:T List. nil = (M @ (x.N))) False |
| 2 | 7. u: T 8. v: T List 9. ( M,N:T List. v = (M @ (x.N))) x(eq) v (M,N:T List. u.v = (M @ (x.N))) if eq(x,u) true else x(eq) v fi |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |