L:T List. 
x
L.P(x) 
False 
x(L @ nil).P(x)4. u: T
5. v: T List
6.
L:T List. xL.P(x) xv.P(x) x(L @ v).P(x) L:T List. xL.P(x) P(u) xv.P(x) x(L @ (u.v)).P(x)
Prop
xL.P(x) xM.P(x)
x(L @ M).P(x)
| 1 | 3. M: T List L:T List. xL.P(x) False x(L @ nil).P(x) |
| 2 | 3. M: T List 4. u: T 5. v: T List 6. L:T List. xL.P(x) xv.P(x) x(L @ v).P(x) L:T List. xL.P(x) P(u) xv.P(x) x(L @ (u.v)).P(x) |
About:
 |  |  |  |  |  |  |  |  |  |