true z(
eq) v
}
T
T
}
x,y:T. f1(x,y) 
eq(x,y)
xv.if eq(x,u)
true else x(eq) v fi 
(z:T. z(f1) v if eq(z,u) true else z(eq) v fi)
f1) v
if eq(z,u) true else z(eq) v fi
| 1 | 12. eq(z,u) = true true |
| 2 | 12. eq(z,u) = false z(eq) v |
About:
 |  |  |  |  |  |
 |  |  |  |  |