At:
list exists is member lemma2211
1.
T: Type
2.
eq: TT
3.
(x,y:T. eq(x,y) x = y) & eq TT
4.
P: TProp
5.
L: T List
6.
u: T
7.
v: T List
8.
yv.P(y) (x:T. x(eq) v & P(x))
9.
P(u)
x:T. x(eq) (u.v) & P(x)
By:
Witness u
THEN
Analyze 0
THEN
Try Trivial
Generated subgoal:
u(
eq) (u.v)
T
x,y:T. eq(x,y) 
x = y) & eq 
y
