S:Sequent, a:Assignment. 
(a |= S & a |
S)
not_sequent_satisfiable_and_falsifiable
S == F
S.H.a |= F & FS.C.a | F
Thm* S:Sequent, a:Assignment. (a |= S & a | S)
not_sequent_satisfiable_and_falsifiable
In prior sections: sequent falsification