eq) v = true
if eq(z,u)
true else z(eq) v 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
if eq(z,u) true else z(eq) v fi
P:. P P = true)
8
| 1 | 8. z(eq) v = true if eq(z,u) true else z(eq) v fi |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |