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
10. L = M
11. u: T
12. v: T List
if eq(u,u)
true
else u(eq) v fi
}
if eq(u,u) true else u(eq) v fi
| 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 10. L = M 11. u: T 12. v: T List if eq(u,u) true else u(eq) v fi |
About:
 |  |  |  |  |  |  |