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: assignment valuation formula satisfaction formula falsification sat lemmas sequent satisfaction sequent falsification sequent sat lemmas full sequent assignment elimination normalization