x
v.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)
xv.if eq(x,u) true else x(eq) v fi
}
T
T
}
x,y:T. f1(x,y) eq(x,y)
xv.if eq(x,u) true else x(eq) v fi
eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z))
[T;f1;
x.if eq(x,u) true else x(eq) v fi;v]
| 1 | 9. 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) xv.if eq(x,u) true else x(eq) v fi |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |