full
sequent
assignment
Sections
ClassicalProps(jlc)
Doc
Def
x
L.P(x) == (letrec list_all L = (Case of L; nil
True ; h.t
P(h) & list_all(t)) ) (L)
In prior sections:
list
3
jlc
x
L.P(x)
== (letrec list_all L = (Case of L; nil 
True ; h.t P(h) & list_all(t)) ) (L)