At:
list exists exists
1
2
1
2
1
1
2
1
1.
T: Type
2.
eq: {T=
}
3.
P: T
Type
4.
L: T List
5.
u: T
6.
v: T List
7.
x
v.P(x) 
(x:{x:T| x(eq) v }. P(x))
8.
xv.P(x) 
(x:{x:T| x(eq) v }. P(x))
9.
xv.P(x)
10.
x: {x:T| x(eq) v }
11.
P(x)
12.
eq(x,u) = true
true
By:
BackThru
Thm* 
P:
. P P = true
Generated subgoals:
None
About:
