T
3. (
x,y:T. eq(x,y) 
x = y) & eq 
TT4. u: T
5. v: T List
6.
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)7. z: T
8. z(
eq) v
if eq(z,u) true else z(eq) v fi}
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
| 1 | 2. eq: TT 3. ( x,y:T. eq(x,y) x = y) & eq TT4. u: T 5. v: T List 6. 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)7. z: T 8. z( eq) v if eq(z,u) true else z(eq) v fi |
About:
 |  |  |  |  |  |  |  |