At:
list exists is member lemma1
1
1
1
1
1.
T: Type
2.
eq: T
T
3.
(
x,y:T. eq(x,y) 
x = y) & eq 
TT
4.
P: TProp
5.
x: T
6.
L: T List
7.
P(x)
x(eq) nil 
ynil.P(y)
By:
Rewrite (HigherC is_member_unrollC THENC HigherC assert_evalC) 0
Generated subgoals:
None
About:
