x,y:T. eq(x,y) 
eq(y,x)5.
x,y,z:T. eq(x,y) 
eq(y,z) eq(x,z)6. L: T List
7. u: T
8. v: T List
9. ||v||
1 hd(v)(
eq) v10. ||u.v||
111. eq(u,u) = false
12. eq(u,u)
u(eq) v
}
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)
1 hd(v)(eq) v
1
u(eq) v
| 1 | 4. x,y:T. eq(x,y) eq(y,x) 5. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)6. L: T List 7. u: T 8. v: T List 9. ||v|| 1 hd(v)(eq) v10. ||u.v|| 111. eq(u,u) = false 12. eq(u,u) u(eq) v |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |
 |