(
z:T. z(
eq) nil 
P(z)) xnil.P(x)8. v: T List
9. (
z:T. z(eq) v P(z)) xv.P(x) (z:T. z(eq) (u.v) P(z)) x(u.v).P(x)
}
T
T
x,y:T. eq(x,y) 
x = y
Prop
z:T. z(eq) L P(z)
xL.P(x)
| 1 | (z:T. z(eq) nil P(z)) xnil.P(x) |
| 2 | 7. u: T 8. v: T List 9. ( z:T. z(eq) v P(z)) xv.P(x) (z:T. z(eq) (u.v) P(z)) x(u.v).P(x) |
About:
 |  |  |  |  |  |  |  |  |  |  |  |  |