x
v.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)
z:T. z(eq) v if eq(z,u) true else z(eq) v fi}
xv.(
z.if eq(z,u) true else z(eq) v fi)(x)
(z:T. z(eq) v (z.if eq(z,u) true else z(eq) v fi)(z))
xv.if eq(x,u) true else x(eq) v fi
| 1 | 5. 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) z:T. z(eq) v if eq(z,u) true else z(eq) v fi |
About:
 |  |  |  |  |  |  |  |  |