At:
list exists exists1211111211
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
P: TType
5.
L: T List
6.
u: T
7.
v: T List
8.
xv.P(x) (x:{x:T| x(eq) v }. P(x))
9.
xv.P(x) (x:{x:T| x(eq) v }. P(x))
10.
P(u)
11.
eq(u,u) = false
12.
eq(u,u) u = u
13.
(eq(u,u)) (u = u)
14.
eq(u,u)
eq(u,u)
}
T
T
x
(
eq(u,u)
