At:
list exists is member lemma11211211
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.
x(eq) (u.v)
12.
eq(x,u)
x(eq) v
By:
Rewrite (HigherC is_member_unrollC) 11
Generated subgoal:
true
else x(
eq) v fi
eq(x,u)
x(
T
x,y:T. eq(x,y) 
x = y) & eq 
y
