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