x
nil.(P(x)) 
xnil.P(x)6. v: T List
7.
xv.(P(x)) xv.P(x) x(u.v).(P(x)) x(u.v).P(x)
Prop
x:T. Dec(P(x))
xL.(P(x))
xL.P(x)
| 1 | xnil.(P(x)) xnil.P(x) |
| 2 | 5. u: T 6. v: T List 7. xv.(P(x)) xv.P(x) x(u.v).(P(x)) x(u.v).P(x) |
About:
 |  |  |  |  |  |  |  |  |