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