At:
list exists is member lemma112112111111
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.
eq(x,u) = true
12.
true
13.
true = false
x(eq) v
By:
ApFunToHypEquands `z' if z 0 else 1 fi 13
THEN
AbReduce -1
Generated subgoals:
T
x,y:T. eq(x,y) 
x = y) & eq 
T
y
x(
0 else 1 fi 
13
