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