At:
list all is member lemma12211111
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
P: TProp
5.
L: T List
6.
u: T
7.
v: T List
8.
(z:T. z(eq) v P(z)) xv.P(x)
9.
z:T. z(eq) (u.v) P(z)
10.
(eq(u,u)) (u = u)
if eq(u,u) true else u(eq) v fi
By:
Assert (u = u) THENL [Auto;Id]
Generated subgoal:
if eq(u,u)
true
else u(
eq) v fi
T
z:T. z(
P(z)) 
