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
nil (
x:T. x(
eq) v)10. u.v
nil11. eq(u,u)
12. eq(u,u) = true
u(eq) (u.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)
nil (x:T. x(eq) v)
nil
u(eq) (u.v)
P:. P P = true
[-1]
| 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 nil (x:T. x(eq) v)10. u.v nil11. eq(u,u) 12. eq(u,u) = true u(eq) (u.v) |
About:
 |  |  |  |  |  |  |  |  |  |  |  |