At:
list exists is member lemma112112111
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.
x: T
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)
x(eq) v
By:
Rewrite
(LemmaC
Thm*P:. P P = false)
12
Generated subgoal:
x(
eq) v
T
x,y:T. eq(x,y) 
x = y) & eq 
y
true
eq(x,u)
