S:Sequent. |= S 
(
a:Assignment. a |
S)
propositional_decidability
a:Full(S). a |= S
Thm* S:Sequent. |= S (a:Assignment. a | S)
propositional_decidability
Thm* S:Sequent. |= S (a:Assignment. a | S) prop_decide
Thm* L:Sequent List.
s
L.(
(s) = 0) 
sL.|= s (a:Assignment. sL.a | s)
zero_rank_valid_or_falsifiable
In prior sections: sequent valid elimination normalization