x,y:T. f1(x,y) 
eq(x,y)
x
v.if eq(x,u)
true
else x(eq) v fi
}
}
xv.if eq(x,u) true else x(eq) v fi
eq:{T=}, f:{T}, x,y:T. eq(x,y) f(x,y)
[T;f1;eq]
| 1 | 8. x,y:T. f1(x,y) eq(x,y) xv.if eq(x,u) true else x(eq) v fi |
About:
 |  |  |  |  |  |  |