At:
list exists exists12211311
1.
T: Type
2.
eq: {T=}
3.
P: TType
4.
L: T List
5.
u: T
6.
v: T List
7.
xv.P(x) (x:{x:T| x(eq) v }. P(x))
8.
xv.P(x) (x:{x:T| x(eq) v }. P(x))
9.
x: T
10.
if eq(x,u) true else x(eq) v fi
11.
P(x)
12.
x = u
x:{x:T| x(eq) v }. P(x)
By:
Witness x
Generated subgoals:
x 
{x:T| x(
}
Type
x
(
true
x = u
