x(
eq) nil 
ynil.P(y)8. u: T
9. v: T List
10. x(
eq) v yv.P(y) x(eq) (u.v) y(u.v).P(y)
T
x,y:T. eq(x,y) 
x = y) & eq TT
Prop
eq) L
yL.P(y)
| 1 | 7. P(x) x(eq) nil ynil.P(y) |
| 2 | 7. P(x) 8. u: T 9. v: T List 10. x( eq) v yv.P(y) x(eq) (u.v) y(u.v).P(y) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |