if f(u,u1)
true
else u(
f) v fi}
T
T
x,y:T. eq(x,y) 
x = y
}
TT
x:T. f(x,x)
x,y:T. f(x,y) f(y,x)
x,y,z:T. f(x,y) 
f(y,z) f(x,z)
eq) v u(f) v
if f(u,u1) true else u(f) v fi
P:. P P = true
[15]
| 1 | 17. eq(u,u1) if f(u,u1) true else u(f) v fi |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |