At:
list exists is member lemma111121121111
1.
T: Type
2.
eq: TT
3.
(x,y:T. eq(x,y) x = y) & eq TT
4.
P: TProp
5.
x: T
6.
L: T List
7.
P(x)
8.
u: T
9.
v: T List
10.
x(eq) v yv.P(y)
11.
if eq(x,u) true else x(eq) v fi
12.
eq(x,u) = false
x(eq) v
By:
HypSubst 12 11
THEN
Rewrite (HigherC ifthenelse_evalC) 11
Generated subgoal:
eq) v
x(
T
x,y:T. eq(x,y) 
x = y) & eq 
y
true
