At:
list exists exists122111111
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.
x: T
11.
if eq(x,u) true else x(eq) v fi
12.
P(x)
13.
eq(x,u) = true
14.
True x = u
15.
True (x = u)
Dec(x = u)
By:
Choose [1]
THEN
HypBackchain
THEN
Trivial
Generated subgoals:
}
T
T
x
(
true
Dec(x = u)
