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. M: T List
L(
eq)M & M(eq)L (
eq)(L,M) & (eq)(M,L)
}
L(eq)M & M(eq)L (((eq)(L,M))
((eq)(M,L)))
p,q:. (pq) p & q))
0
| 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. M: T List L(eq)M & M(eq)L (eq)(L,M) & (eq)(M,L) |
About:
 |  |  |  |  |