if eq(z,u)
true
else true fi
T
x,y:T. eq(x,y) 
x = y) & eq 
TT
xv.if eq(x,u) true else x(eq) v fi 
(z:T. z(eq) v if eq(z,u) true else z(eq) v fi)
eq) v = true
if eq(z,u) true else z(eq) v fi
| 1 | if eq(z,u) true else true fi |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |