At:
not list all not iff list exists1121112
1.
T: Type
2.
P: TProp
3.
L: T List
4.
u: T
5.
v: T List
6.
xv.(P(x)) xv.P(x)
7.
(P(u) & xv.(P(x)))
8.
(P(u) & xv.(P(x))) P(u) xv.(P(x))
9.
P(u)
P(u) xv.P(x)
By:
Choose [2]
THEN
HypBackchain
Generated subgoal:
x
v.(
Prop
x
