At:
list all is member lemma1221111111
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)
11.
u = u
12.
eq(u,u)
13.
eq(u,u) = true
if eq(u,u) true else u(eq) v fi
By:
HypSubst 13 0
THEN
Rewrite (HigherC ifthenelse_evalC THENC assert_evalC) 0
THEN
Trivial
Generated subgoals:
}
T
T
z:T. z(
P(z)) 
if eq(u,u)
true
