At:
list exists append lemma22121221
1.
T: Type
2.
P: TProp
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)
7.
L: T List
8.
u1: T
9.
v1: T List
10.
xv1.P(x) P(u) xv.P(x) x(v1 @ (u.v)).P(x)
11.
xv.P(x)
xv1.P(x) P(u) xv.P(x)
By:
Choose [2;2]
THEN
Trivial
Generated subgoals:
Prop
L:T List. 
x
L.P(x) 
