if eq(z,u)
true
else z(
eq) v fi 
z(eq) L3
}
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)
}
TT
x,y:T. f(x,y) x = y
f) L1
z:T. z(f) v z(eq) L3) z(eq) v z(eq) L3
z:T. z(f) (u.v) z(eq) L3
eq) (u.v)
z(eq) L3
| 1 | if eq(z,u) true else z(eq) v fi z(eq) L3 |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |