list
3
jlc
Sections
Support(jlc)
Doc
Theorem
Name
Thm*
P:(T
Prop), L:T List. (
x:T. Dec(P(x)))
Dec(
x
L.P(x))
[decidable__list_all]
cites
Thm*
Dec(P)
Dec(Q)
Dec(P & Q)
[decidable__and]
list
3
jlc
Sections
Support(jlc)
Doc