At:
not list all 2 implies exists not1211111111
1.
T: Type
2.
eq: {T}
3.
P: T
4.
L: T List
5.
u: T
6.
v: T List
7.
xv.P(x) (x:{x:T| x(eq) v }. P(x))
8.
(P(u) & xv.P(x))
9.
(P(u) & xv.P(x)) P(u) xv.P(x)
10.
P(u)
eq(u,u) = true
By:
BackThru
Thm*P:. P P = true
THEN
BackThru
Thm*eq:{T}, u:T. eq(u,u)
Generated subgoals:
}
x
(
x:{x:T| x(
eq(u,u) = true
