(23steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
not
list
all
not
iff
list
exists
T:Type, P:(T
Prop). (
x:T. Dec(P(x)))
(
L:T List.
x
L.(
P(x))
x
L.P(x))
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
P:
T
Prop
3.
x:T. Dec(P(x))
4.
L:
T List
x
L.(
P(x))
x
L.P(x)
About:
(23steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
Prop
x:T. Dec(P(x))
x
L.(P(x)) 
xL.P(x)
T:Type, P:(TProp). (x:T. Dec(P(x))) 
(L:T List. xL.(P(x)) xL.P(x))
Propx:T. Dec(P(x)) xL.(P(x)) xL.P(x)
