At:
list all is member lemma122121111
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
x,y:T. eq(x,y) x = y
5.
P: TProp
6.
L: T List
7.
u: T
8.
v: T List
9.
(z:T. z(eq) v P(z)) xv.P(x)
10.
z:T. z(eq) (u.v) P(z)
11.
z: T
12.
z(eq) v
if eq(z,u) true else z(eq) v fi
By:
GenConcl (eq(z,u) = b)
THEN
BoolInd -2
THEN
Rewrite (HigherC ifthenelse_evalC THENC TryC assert_evalC) 0
THEN
Try Trivial
Generated subgoals:
}
T
T
x,y:T. eq(x,y) 
x = y
if eq(z,u)
true
