L = (nil @ (u.N)) 
(
v:T, M:T List. L = v.M)11. v: T List
12. L = (v @ (u.N))
(v:T, M:T List. L = v.M) L = ((u1.v) @ (u.N)) (v:T, M:T List. L = v.M)
}
T
T
x,y:T. eq(x,y) 
x = y
eq) L
v:T, M:T List. L = v.M
| 1 | L = (nil @ (u.N)) (v:T, M:T List. L = v.M) |
| 2 | 10. u1: T 11. v: T List 12. L = (v @ (u.N)) (v:T, M:T List. L = v.M) L = ((u1.v) @ (u.N)) (v:T, M:T List. L = v.M) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |