At:
list exists is member lemma2212111
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.
u: T
7.
v: T List
8.
x: yv.P(y)
9.
x1: T
10.
x1(eq) v
11.
P(x1)
x1(eq) (u.v)
By:
Rewrite (HigherC is_member_unrollC) 0
THEN
GenConcl (eq(x1,u) = b)
THEN
BoolInd -2
THEN
Rewrite (HigherC ifthenelse_evalC THENC TryC (HigherC assert_evalC)) 0
THEN
Try Trivial
Generated subgoals:
T
x,y:T. eq(x,y) 
x = y) & eq 
T
y
x1(