T
T
5.
x:T. eq(x,x)6.
x,y:T. eq(x,y) 
eq(y,x)7.
x,y,z:T. eq(x,y) 
eq(y,z) eq(x,z)8. L: T List
9. u: T
10. v: T List
11.
M:T List. v(
eq)M (
eq)(v,M)12. M: T List
u(eq) M & v(eq)M (u(eq) M
xv.x(eq) M)
}
M:T List. v(eq)M (eq)(v,M)
(u.v)(eq)M (eq)(u.v,M)
| 1 | 4. eq TT 5. x:T. eq(x,x)6. x,y:T. eq(x,y) eq(y,x)7. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)8. L: T List 9. u: T 10. v: T List 11. M:T List. v(eq)M (eq)(v,M)12. M: T List u(eq) M & v(eq)M (u(eq) Mxv.x(eq) M) |
About:
 |  |  |  |  |  |  |