Thm* a:Assignment, S:Sequent. SqStable(a |
S)
sq_stable__sequent_falsifiable
Thm* S:Sequent, a:Assignment. Dec(a |
S)
decidable__sequent_falsifiable
In prior sections: assignment valuation formula satisfaction formula falsification sat lemmas sequent satisfaction