list
3
jlc
Sections
Support(jlc)
Doc
Theorem
Name
Thm*
L:T List, P:(T
).
x
L.P(x)
x
L.P(x)
[list_all_iff_assert_list_all_2]
cites
Thm*
p,q:
. (p
q)
p & q
[assert_of_band]
list
3
jlc
Sections
Support(jlc)
Doc
L:T List, P:(T
). x
L.P(x) 
x
L.P(x)p,q:. (p
q) p & qL:T List, P:(T). xL.P(x) xL.P(x)p,q:. (pq) p & q