At:
list exists is member lemma2211111111
1.
T: Type
2.
eq: TT
3.
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)
10.
eq(u,u)
11.
eq(u,u) = true
if eq(u,u) true else u(eq) v fi
By:
HypSubst 11 0
THEN
Rewrite (HigherC ifthenelse_evalC THENC HigherC assert_evalC) 0
THEN
Trivial
Generated subgoals:
T
T
y
(
if eq(u,u)
true
