{T}

eq TT

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(x,u) = false

x(eq) v

M,N:T List, y:T. eq(x,y) & v = (M @ (y.N))

M,N:T List, y:T. eq(x,y) & u.v = (M @ (y.N))

1	13. M: T List 14. N: T List 15. y: T 16. eq(x,y) 17. v = (M @ (y.N)) M,N:T List, y:T. eq(x,y) & u.v = (M @ (y.N))

About: