L:Sequent List.
s
L.(
(s) = 0) 
sL.|= s 
(
a:Assignment. sL.a |
s)
zero_rank_valid_or_falsifiable
xL.P(x)
== (letrec list_exists L = (Case of L; nil 
False ; h.t P(h) list_exists(t)) ) (L)
Thm* L:Sequent List.
sL.((s) = 0)
sL.|= s (a:Assignment. sL.a | s)
zero_rank_valid_or_falsifiable
In prior sections: list 3 jlc sequent rank normalization