Thm* a:Assignment, S:Sequent. SqStable(a |= S) sq_stable__sequent_satisfiable

Thm* S:Sequent, a:Assignment. Dec(a |= S) decidable__sequent_satisfiable

In prior sections: assignment valuation formula satisfaction formula falsification sat lemmas