Thm* S:Sequent, a:Assignment. (a |= S & a | S) not_sequent_satisfiable_and_falsifiable
In prior sections: assignment valuation formula satisfaction formula falsification sat lemmas sequent satisfaction sequent falsification