S:Sequent. |= S 
(
a:Assignment. a |
S)
propositional_decidability
S == F
S.H.a |= F & FS.C.a | F
Thm* S:Sequent. |= S (a:Assignment. a | S)
propositional_decidability
Thm* S:Sequent. |= S (a:Assignment. a | S) prop_decide
Thm* L:Sequent List.
sL.(
(s) = 0) 
sL.|= s (a:Assignment. sL.a | s)
zero_rank_valid_or_falsifiable
In prior sections: sequent falsification sequent sat lemmas full sequent assignment elimination normalization