true
else z(
eq) v fi14.
eq(z,u)15. eq(z,u) = false
z(eq) v}
T
T
x,y:T. eq(x,y) 
x = y
Prop
xv.P(x) 
z(eq) v P(z)
xv.P(x)
eq) (u.v)
eq(z,u)
z(eq) v
P:. P P = false
[14]
| 1 | 13. if eq(z,u) true else z(eq) v fi 14. eq(z,u)15. eq(z,u) = false z(eq) v |
About:
 |  |  |  |  |  |  |  |  |  |  |  |