Thm* S:Sequent, a:Assignment. (a |= S & a | S) not_sequent_satisfiable_and_falsifiable

In prior sections: core bool 1 rel 1 sqequal 1 prog 1 int 2 list 1 bool 2 jlc core 3 jlc list 3 jlc Three assignment sat lemmas sequent rank