sequent sat lemmas Sections ClassicalProps(jlc) Doc

Def Sequent == (Formula List)(Formula List)

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

In prior sections: sequent sequent equality sequent rank sequent satisfaction sequent falsification