x
v.(
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}
xv.if eq(x,u) true else x(eq) v fi
eq:{T=}, P:(T
Prop), L:T List. xL.P(x) (z:T. z(eq) L P(z))
[T;eq;z.if eq(z,u) true else z(eq) v fi;v]
THENL
[Auto;Auto;Analyze 2;Auto;Id]
| 1 | 5. 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 |
About:
 |  |  |  |  |  |  |