x,y:T. eq(x,y) 
eq(y,x)6.
x,y,z:T. eq(x,y) 
eq(y,z) eq(x,z)7. L: T List
8. M: T List
9. L = M
10. u: T
11. v: T List
12. eq(u,u)
13. eq(u,u) = true
if eq(u,u)
true else u(
eq) v fi
}
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)
if eq(u,u) true else u(eq) v fi
P:. P P = true
[-1]
| 1 | 5. x,y:T. eq(x,y) eq(y,x) 6. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)7. L: T List 8. M: T List 9. L = M 10. u: T 11. v: T List 12. eq(u,u) 13. eq(u,u) = true if eq(u,u) true else u(eq) v fi |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |